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

next up previous contents index
Next: The Typed Lambda Up: No Title Previous: Systems Background

Introduction to Type Theory

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.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995