The People's Refinement Logic

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



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


Jon Sterling, Kuen-Bang Hou (Favonia), James Wilcox, Danny Gratzer, Darin Morrison, David Christiansen, Eugene Akentyev and Ayberk Tosun contributed to the design and implementation of RedPRL.