Also see Nuprl Basics and Naive Type Theory for newer supplementary material.

Sections 2.1 to 2.4 introduce a sequence of
approximations to Nuprl
, starting with a familiar formalism,
the * typed lambda calculus*. These approximations are not exactly
subsets of Nuprl
, but the differences between these theories and
subtheories of
are minor. These
subsections take small steps toward the full theory and relate
each step to familiar ideas. Section 2.5 summarizes the main ideas
and can be used as a starting point for readers who want a brief
introduction. The last two sections relate the idea of a type in
Nuprl
to the concept of a set and to the concept of a data type in
programming languages.

- The Typed Lambda Calculus
- Extending the Typed Lambda Calculus
- Equality and Propositions as Types
- Sets and Quotients
- Semantics
- Relationship to Set Theory
- Relationship to Programming Languages

Thu Sep 14 08:45:18 EDT 1995