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…