2 papers
cs.LO2026
Nominal Type Theory by Nullary Internal Parametricity
Antoine Van Muylder, Andreas Nuyts, Dominique Devriese
There are many ways to represent the syntax of a language with binders. In particular, nominal frameworks are metalanguages that feature (among others) name abstraction types, whic…
cs.PL2025
Towards Computational UIP in Cubical Agda
Yee-Jian Tan, Andreas Nuyts, Dominique Devriese
Some advantages of Cubical Type Theory, as implemented by Cubical Agda, over intensional Martin-Löf Type Theory include Quotient Inductive Types (QITs), which exist as instances o…