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 language | English (US) |
|---|---|
| Pages (from-to) | 1-10 |
| Number of pages | 10 |
| Journal | Electronic Proceedings in Theoretical Computer Science, EPTCS |
| Volume | 274 |
| DOIs | |
| State | Published - Jul 3 2018 |
| Event | 13th 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.
Publisher Copyright:
© Angiuli, Cavallo, Hou (Favonia), Harper, Sterling