RedPRL is a proof assistant for Computational Cubical Type Theory being developed at Carnegie Mellon University by Jon Sterling under Robert Harper, inspired by Nuprl.
Open-source contributors are the shock troops of the revolution! Join us now.
Papers & Talks
- Sterling, Harper. Algebraic Foundations of Proof Refinement. Draft, 2016.
- Angiuli, Harper, Wilson. Computational Higher-Dimensional Type Theory. POPL 2017.
- Strict / exact equality
- Identification (path) types
- Functional extensionality
- Dependent proof refinement
- Well-scoped tactic scripts
DownloadRedPRL is written in Standard ML, and is available for download on GitHub.
Jon Sterling, Kuen-Bang Hou (Favonia), James Wilcox, Danny Gratzer, Darin Morrison, David Christiansen, Eugene Akentyev and Ayberk Tosun contributed to the design and implementation of RedPRL.