4 papers
Cubical Syntax for Reflection-Free Extensional Equality
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
We contribute XTT, a cubical reconstruction of Observational Type Theory which extends Martin-Löf's intensional type theory with a dependent equality type that enjoys function exte…
The RedPRL Proof Assistant (Invited Paper)
Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou +2
RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type the…
Computational Higher Type Theory III: Univalent Universes and Exact Equality
Carlo Angiuli, Kuen-Bang Hou, Robert Harper
This is the third in a series of papers extending Martin-Löf's meaning explanations of dependent type theory to a Cartesian cubical realizability framework that accounts for higher…
Computational Higher Type Theory I: Abstract Cubical Realizability
Carlo Angiuli, Robert Harper, Todd Wilson
Brouwer's constructivist foundations of mathematics is based on an intuitively meaningful notion of computation shared by all mathematicians. Martin-Löf's meaning explanations for…