4 papers · 1 filter
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…
A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report
Joris Ceulemans, Andreas Nuyts, Dominique Devriese
This is the technical report accompanying the paper "A Sound and Complete Substitution Algorithm for Multimode Type Theory" [Ceulemans, Nuyts and Devriese, 2024]. It contains a ful…
Transpension: The Right Adjoint to the Pi-type
Andreas Nuyts, Dominique Devriese
Presheaf models of dependent type theory have been successfully applied to model HoTT, parametricity, and directed, guarded and nominal type theory. There has been considerable int…
The Transpension Type: Technical Report
Andreas Nuyts
The purpose of these notes is to give a categorical semantics for the transpension type (Nuyts and Devriese, Transpension: The Right Adjoint to the Pi-type, Accepted at LMCS, 2024)…