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. Cubical RedPRL: The People's Refinement Logic. CMU PL Lunch, 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.
History & Philosophy
negation of formalism consists in
decisively overthrowing the old intensional order of truth-as-derivability, and the
reversal of 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.
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.
Jon Sterling, James Wilcox, Danny Gratzer, Darin Morrison, David Christiansen, Eugene Akentyev and Ayberk Tosun contributed to the design and implementation of RedPRL.