Some Lambda Calculus and Type Theory Formalized

James McKinna
Robert Pollack

December 1997


In previous papers we have used the LEGO proof development system to formalize and check a substantial body of knowledge about lambda calculus and type theory. 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

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.