Showing cs.PLShow all
2 papers · 1 filter
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…
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)…