On the Correspondence Between Proofs and Lambda-Terms
The correspondence between natural deduction proofs and λ-terms is presented and discussed. A variant of the reducibility method is presented, and a general theorem for establishing properties of typed (first-order) λ-terms is proved. As a corollary, we obtain a simple proof of the Church-Rosser property, and of the strong normalization property, for the typed λ-calculus associated with the system of (intuitionistic) first-order natural deduction, including all the connectors →, ×, +, ∀,∃ and ⊥ (falsity) (with or without η-like rules). Comments University of Pennsylvania Department of Computer and Information Science Technical Report No. MSCIS-93-01. This technical report is available at ScholarlyCommons: http://repository.upenn.edu/cis_reports/418 On the Correspondence Between Proofs and A-Terms MS-CIS-93-01 LOGIC & COMPUTATION 54