Highlights

Section 2 stresses a typed presentation of the predicate calculus because we deal with a general mechanism for making the judgment that a formula is meaningful. This is done first in the style of Martin-Löf as expressed in Nuprl, but I also mention the essential novelty in Nuprl's use of direct computation rules which go beyond Martin-Löf's inference rules by allowing reasoning about general recursive functions (say defined by the Ycombinator). This is a powerful mechanism that is not widely known.

Section 2 also stresses the notion that proof expressions are sensible for classical logic (see [30]). This separates an important technique from its origins in constructive logic. So the account of Typed Logic covers both constructive as well as classical logic. It also lays the ground work for tactics.

Section 3 features a very simple fragment of type theory which illustrates the major design issues. The fragment has a simple (predicative) inductive semantics. We keep extending it until the semantics requires the insights from [2].

The treatment of recursive types in Section  is quite simple because it deals only with partial types. It suggests that just as the notion of program ``correctness'' can be nicely factored into partial and total correctness, the rules for data types can also be factored this way.

 

Table: Type concepts

Typed Logic	Type Theory	Typed Programming
terms with binding	terms with binding	terms with binding
definitional equality	computation rules	observational equivalence &
		bisimulation
proofs as objects	content of proofs	programs
$P\!rop_i$	$T\!ype_i$ or Ui	$T\!ype$ (partial types)
equality propositions	equality judgments	equality functions
consistency	nontriviality	representation integrity
		(internal & external)
standard models	inductive definitions	termination conditions
proof synthesis	element synthesis	program synthesis
tactic-tree proof	derivation	proof data type & tactics

 

Table 1 shows how similar concepts change their appearance as they are situated in the three different contexts.