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, James Wilcox, Danny Gratzer, Darin Morrison, David Christiansen, Eugene Akentyev and Ayberk Tosun contributed to the design and implementation of RedPRL.