The RedPRL proof assistant (invited paper)

Carlo Angiuli, Evan Cavallo, Kuen Bang Hou Favonia, Robert Harper, Jonathan Sterling

Research output: Contribution to journalConference article

2 Scopus citations


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 theory. In the style of Nuprl, RedPRL users employ tactics to establish behavioral properties of cubical functional programs embodying the constructive content of proofs. Notably, RedPRL implements a two-level type theory, allowing an extensional, proof-irrelevant notion of exact equality to coexist with a higher-dimensional proof-relevant notion of paths.

Original languageEnglish (US)
Pages (from-to)1-10
Number of pages10
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
StatePublished - Jul 3 2018
Externally publishedYes
Event13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2018 - Oxford, United Kingdom
Duration: Jul 7 2018 → …

Cite this