Formalizing Type Theory

Nuprl presents a particular formalization of type theory. There are several others [17,22,23,24,26,42]. At the core are ideas from deBruijn [17] and Martin-Löf [34] extended with the notions of inductive types and direct computation which give Nuprl its unique architecture.

The formalization comes in two parts. First we lay down the structure of terms and then evaluation.

This is the functional programming core of the theory, on top of it, we define the notion of type and proof. These are the basis of logic and mathematics.