Fancy new name binding technique just dropped: arxiv.org/abs/2512.09464 (work by Antoine van Muylder, @anuytstt and Dominique Devriese).

It includes such things as nominal pattern matching and synthetic Kripke parametricity. It's even implemented as an extension to "the mature proof assistant Agda"! [EDIT: actually it's only the older binary version that has been implemented, not this nullary version.] Disclaimer: I haven't read the paper yet, but this sounds very cool.

#TypeTheory #NameBinding #Parametricity #Agda