Curry–Howard Correspondence
IMPERIAL COLLEGE PRESS eBooks · 2011
Outside of logic, computer science, and mathematics, the Curry-Howard correspondence is ordinarily described as a deep connection between proofs and programs.However, without sufficient requisite background knowledge, such a description can be mystifying and contribute to the correspondence's general obscurity.In this thesis, we attempt to introduce the Curry-Howard correspondence by presenting an elementary correspondence between the extended simply-typed lambda calculus and intuitionistic natural deduction.Our introduction aims to provide the necessary theoretical background to understand the basic correspondence, which can help bridge the gap between non-specialists and the more advanced literature on the topic.Such an introduction also serves to better demonstrate and clarify the correspondence's significance, which is a topic we explore towards the end.To introduce the correspondence, we introduce the lambda calculus and the simply-typed lambda calculus.Moreover, we introduce natural deduction and subsequently develop a novel sequent-style natural deduction for reasons philosophical as well as logically advantageous.As a result, we methodically prove a full isomorphism between our system of natural deduction and the extended simply-typed lambda calculus.