The RedPRL Proof Assistant (Invited Paper)

Carlo Angiuli
Evan Cavallo
Kuen-Bang Hou (Favonia)
Robert Harper
Jonathan Sterling

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.

In Frédéric Blanqui and Giselle Reis: Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2018), Oxford, UK, 7th July 2018, Electronic Proceedings in Theoretical Computer Science 274, pp. 1–10.
Published: 3rd July 2018.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: