*From the introduction:*

``This paper is about our hobby.'' That is the first sentence of
the first report on our formal development of lambda calculus and
type theory, written in autumn 1992. We have continued to pursue
this hobby on and off ever since, and have developed a substantial
body of formal knowledge, including Church-Rosser and
standardization theorems for beta reduction, and the basic theory
of Pure Type Systems (**PTS**) leading to the strengthening
theorem and type checking algorithms for **PTS**. This work is
reported in the second author's PhD thesis and elsewhere. In the
present paper we survey this work, including some new proofs, and
point out what we feel has been learned about the general issues of
formalizing mathematics. On the technical side, we describe an
abstract, and simplified, proof of standardization for beta
reduction, not previously published, that does not mention redex
positions or residuals. On the general issues, we emphasize the
search for formal definitions that are convenient for formal proof
and convincingly represent the intended informal concepts.

The LEGO Proof Development System was used to check the work in an implementation of the Extended Calculus of Constructions (ECC) with inductive types. LEGO is a refinement style proof checker, publicly available by ftp and WWW, with a User's Manual and a large collection of examples. Interesting examples formalized in LEGO include program specification and data refinement, strong normalization of System F, synthetic domain theory, operational semantics for imperative programs and the formal development described in this paper.

This report is available in the following formats:

- PDF file
- Gzipped PDF file
- PostScript file
- Gzipped PostScript file
- PostScript file with Type 1 fonts
- Gzipped PostScript file with Type 1 fonts
- LaTeX DVI file
- Gzipped LaTeX DVI file