Red**PRL** 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.
- Sterling. Cubical RedPRL: The People's Refinement Logic. CMU PL Lunch, 2016.
- Angiuli, Harper, Wilson. Computational Higher-Dimensional Type Theory. POPL 2017.

# Features

- Strict / exact equality
- Identification (path) types
- Functional extensionality
- Dependent proof refinement
- Well-scoped tactic scripts

# Download

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

# History & Philosophy

The first ~~negation~~ of formalism consists in
decisively abolishing the old intensional order of truth-as-derivability, and reversing the prior relations between meaning theory and proof theory. The meaning
explanation is both concrete and definitive, and proof
theory is no longer a classifier of models, but a mere
means of implementation.

In a of the ~~negation~~~~negation~~,
the standard semantics are generalized to a theory of Kripke logical
relations to account for transcendental phenomena, including continuity and higher dimension. The purely formal negative freedom
accorded by the toppled edifice is replaced with a living open-endedness,
emanating from the free generation of fresh objects.

# Contributors

Jon Sterling, James Wilcox, Danny Gratzer, Darin Morrison, David
Christiansen, Eugene Akentyev and Ayberk Tosun contributed to the
design and implementation of Red**PRL**.