3 papers
cs.LO2018
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…
cs.LO2017
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…
cs.LO2016
A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory
Kuen-Bang Hou, Eric Finster, Dan Licata +1
This paper continues investigations in "synthetic homotopy theory": the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory We present…