Red**PRL** 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.

# Features

- computational canonicity and extraction
- univalence as a theorem
- strict / exact equality types
- coequalizer and pushout types
- functional extensionality
- equality reflection
- proof tactics

# Download

Red**PRL**is written in Standard ML, and is available for download on GitHub.

# Contributors

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
Red**PRL**.