Outline

Section 2 covers Typed Logic. The development moves from a pure logic of typed propositions to a calculus with specific types-- ${{\mathbb{N} }}$ the natural numbers, cartesian products of types, lists over any types, functions from one type to another, sets built over a type, and types defined by imposing a new equality on our existing type...so called quotient or congruence types.

The exposition is very similar to the way logic is presented in Nuprl, but instead of deriving logic from type theory, we start with logic in the spirit of Principia. We also present logic in the manner of Automath, so one might call this logic ``AutoMathematica.'' It contrasts with the polymorphic predicate calculus of LCF ([55]) and HOL ([54]).

Section 3 covers Type Theory. This is essentially an introduction to Martin-Löf semantics using an axiomatic theory close to his Intuitionistic Type Theory circa 1982-88 and its Nuprl variants ([80,82,81]). My approach is very ``expository'' since there are many accessible accounts in the books of [89,82,112], the articles of [5,80,2], and the theses of [3,92,93,96,106,103,59] which provide technical detail. I use a small fragment to illustrate the theory and present Stuart Allen's non-type theoretic account [2] as well as a semantics of proofs as objects. Many of the ideas of type theory are discussed for the impredicative theories based on Girard's system F(see [50]). There is a large literature here as well [37,102,77,96]. Dependent types and universes are in this section. These types can then be added to the Typed Logic. So in a sense, this section extends Typed Logic.

Section  covers Typed Programming. Here I explain the notion of ``partial types'' common in programming and relate them to type theory. This account is expository, designed to make connections. But I discuss the recursive types that [34] introduced which are closely related to the subsequent accounts for Coq and Alf of [38,41]. I then discuss a new type constructor due to Jason Hickey [60] -- the very dependent type. These recursive and very dependent types can be added to the type theory and hence, to the Typed Logic. So this section too can be viewed as extending the logic of Section 2. This section provides the theoretical basis for understanding tactic-oriented proving, but there is no space to treat the subject further.