The People’s Refinement Logic

RedPRL is a new proof assistant in the Nuprl tradition for Nominal Computational Type Theory.

Open-source contributors are the shock troops of the revolution! Join us now.

Features

History & Philosophy

The first 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.

In a negation of the negation, the standard semantics are generalized to a theory of Kripke logical relations to account for transcendental phenomena, including continuity.

Then, the reactionary notion of «nonstandard model» is reflected in the new order as a «non-initial world», and the open-endedness of formal hypothetical judgment, formerly an impediment to the equality of objects under assumption, is restored in harmony with the new order.

Contributors

Jon Sterling, Danny Gratzer, Vincent Rahli, Darin Morrison, David Christiansen and Eugene Akentyev contributed to the design and implementation of Classic JonPRL and RedPRL.