# nLab NuPRL

Contents

### Context

#### Constructivism, Realizability, Computability

intuitionistic mathematics

# Contents

## Idea

The dialect of intuitionistic type theory used is also referred to as computational type theory.

The PRL part of the name evidently stands for “Proof Refinement Logic”.

## Descendants

• MetaPRL: A logical framework implementation that includes (an old version of) Nuprl’s logic as a theory, and focuses on an efficient, modular tactic engine for proof automation.

• RedPRL: An experimental proof assistant for a cubical variant of computational type theory.

• Prototype CompLF: A tentative design for a modern, minimalistic variant of Nuprl’s logic, with an emphasis on internally reflecting the semantic judgments.

proof assistants:

based on plain type theory/set theory:

projects for formalization of mathematics with proof assistants:

Historical projects that died out:

## References

• Robert Constable, Stuart F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, James T. Sasaki, and Scott F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, NJ, 1986.

• Innovations in Computational Type Theory using Nuprl (pdf)

Last revised on October 10, 2020 at 13:28:54. See the history of this page for a list of all contributions to it.