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.
- Functional extensionality
- Squash and subset types
- Computational congruence
- Dependent refinement
- Well-scoped tactic scripts
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.
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.
Jon Sterling, Danny Gratzer, Vincent Rahli, Darin Morrison, David Christiansen and Eugene Akentyev contributed to the design and implementation of Classic JonPRL and RedPRL.