**Robert L. Constable
Cornell University**

This article approaches the subject of modern type theory from the familiar
territory of logic. It starts with an account of pure *typed predicate
logic* which is similar to the ordinary predicate calculus except that
judgments of whether an expression is meaningful are explicit, and proofs are
treated as mathematical objects (as opposed to metamathematical ones).

The pure typed predicate logic is extended with concrete types and type
constructors creating an type theory. This theory is related back to
*Principia Mathematica* and forward to modern proof development systems
like NuprlNuprl (``new pearl''). The semantic basis of this
theory is taken to be Martin-Löf's ``inductive semantics'' as opposed to
Tarski's truth-value semantics.

The last section looks at the type systems of programming languages from the viewpoint of Martin-Löf semantics. Programming types are seen as ``partial types'', and their theories are considered to be partial axiomatizations of mathematical types. The point is illustrated mainly for recursive types. The notion that is also explored.

- Introduction
- Typed logic
- Type theory
- Bibliography
- About this document ...