Abstract

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.