Showing 2024Show all
3 papers · 1 filter
cs.PL2024
On the Semantic Expressiveness of Iso- and Equi-Recursive Types
Dominique Devriese, Eric Mark Martin, Marco Patrignani
Recursive types extend the simply-typed lambda calculus (STLC) with the additional expressive power to enable diverging computation and to encode recursive data-types (e.g., lists)…
cs.LO2024
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…
cs.LO2024
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…