RedPRL is a proof assistant for Computational Higher-Dimensional Type Theory being developed at Carnegie Mellon University by the RedPRL Development Team under the supervision of Robert Harper, inspired by Nuprl.
Open-source contributors are the shock troops of the revolution! Join us now.
Papers & Talks
- Harper, Angiuli. Computational (Higher) Type Theory. ACM POPL Tutorial Session 2018.
- Kuen-Bang Hou (Favonia). Computational Higher-Dimensional Type Theory & RedPRL. Big Proof 2017.
- Angiuli, Harper, Wilson. Computational Higher-Dimensional Type Theory. POPL 2017.
- Sterling, Harper. Algebraic Foundations of Proof Refinement. Draft, 2016.
- computational canonicity and extraction
- univalence as a theorem
- strict / exact equality types
- coequalizer and pushout types
- functional extensionality
- equality reflection
- proof tactics
DownloadRedPRL is written in Standard ML, and is available for download on GitHub.
RedPRL is developed by Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou (Favonia) and Jon Sterling under the supervision of Robert Harper. Full Contributors.
This research was sponsored by the Air Force Office of Scientific Research under grant number FA9550-15-1-0053 and the National Science Foundation under grant number DMS-1638352. We also 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 the 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.