19 citations · 44 across the 8 of their papers we have counts for
Showing 2018 · cs.LOShow all
2 papers · 2 filters
cs.LO2018★ 5 cited
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.LO2018★ 12 cited
Computational Higher Type Theory IV: Inductive Types
Evan Cavallo, Robert Harper
This is the fourth in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to higher-dimensional types. In this installment, we show how to define…