Some Lambda Calculus and Type Theory Formalized

James McKinna, Randy Pollack

Research output: Contribution to journalArticlepeer-review

74 Citations (Scopus)


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 meta theory 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.

Original languageEnglish
Pages (from-to)373-409
Number of pages37
JournalJournal of Automated Reasoning
Issue number3
Publication statusPublished - Nov 1999


  • Formal mathematics
  • Lambda calculus
  • LEGO proof checker
  • Pure Type Systems
  • Type theory

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence


Dive into the research topics of 'Some Lambda Calculus and Type Theory Formalized'. Together they form a unique fingerprint.

Cite this