The People's Refinement Logic

RedPRL 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

Features

Download

RedPRL 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 RedPRL.