RedPRL is a proof assistant for Computational Higher-Dimensional Type Theory being developed at Carnegie Mellon University by Jon Sterling and others 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.
Jon Sterling, Kuen-Bang Hou (Favonia), Evan Cavallo, Carlo Angiuli, James Wilcox, Eugene Akentyev, David Christiansen, Daniel Gratzer and Darin Morrison have contributed to the design and implementation of RedPRL.