Post #872115
2025-12-15 09:47 UTC
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
Replies (3)
-
@jesper@agda.club 2025-12-15 09:50
@anuytstt apparently I'm 4 days late already mastoxiv.page/@arXiv_csLO_bot/115699812365501592
-
@jaror@social.edu.nl 2025-12-15 10:32
@jesper @anuytstt I'm lost at this sentence in the introduction: > For example the parametricity of a function f : A → B is a proof that f maps related inputs in A to related outputs in B, i.e. f is a morphism of reflexive graphs. Which relations on A and B are we talking about?
-
@avmu@mathstodon.xyz 2025-12-15 12:56
@jesper @anuytstt Thanks for the shoutout! Currently there is no implementation of this theory