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

- Functional extensionality
- Squash and subset types
- Computational congruence
- Dependent refinement
- Well-scoped tactic scripts

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

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