The RedPRL proof assistant (invited paper)

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

Research output: Contribution to journalConference articlepeer-review

2 Scopus citations

Abstract

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
Volume274
DOIs
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 → …

Bibliographical note

Funding Information:
This research was sponsored by the National Science Foundation under grant number DMS-1638352 and the Air Force Office of Scientific Research under grant number FA9550-15-1-0053. The second author would also like to thank the Isaac Newton Institute for Mathematical Sciences for its support and hospitality during the program “Big Proof” when part of work on this paper was undertaken; the program was supported by Engineering and Physical Sciences Research Council under grant number EP/K032208/1. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of any sponsoring institution, government or any other entity.

Cite this