McKinna, James; Pollack, Robert Some lambda calculus and type theory formalized. (English) Zbl 0940.03019 J. Autom. Reasoning 23, No. 3-4, 373-409 (1999). Summary: We survey a substantial body of knowledge about lambda calculus and Pure Type Systems, formally developed in a constructive type theory using the LEGO proof system. On lambda calculus, we work up to an abstract, simplified proof of standardization for beta reduction that does not mention redex positions or residuals. Then we outline the metatheory of Pure Type Systems, leading to the strengthening lemma. One novelty is our use of named variables for the formalization. Along the way we point out what we feel has been learned about general issues of formalizing mathematics, emphasizing the search for formal definitions that are convenient for formal proof and convincingly represent the intended informal concepts. Cited in 25 Documents MSC: 03B40 Combinatory logic and lambda calculus 03B35 Mechanization of proofs and logical operations 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:formal mathematics; LEGO proof checker; pure type systems; survey; lambda calculus; constructive type theory; standardization for beta reduction; formal definitions; formal proof Software:LEGO; Automath; Coq PDFBibTeX XMLCite \textit{J. McKinna} and \textit{R. Pollack}, J. Autom. Reasoning 23, No. 3--4, 373--409 (1999; Zbl 0940.03019) Full Text: DOI