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



RedPRL is written in Standard ML, and is available for download on GitHub.


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.