The Curry-Howard Correspondence

Simple item page
dc.contributor.advisorZach, Richard
dc.contributor.authorFarooqui, Husna
dc.contributor.committeememberWyatt, Nicole
dc.contributor.committeememberFantl, Jeremy
dc.date2021-11
dc.date.accessioned2021-08-17T20:25:18Z
dc.date.available2021-08-17T20:25:18Z
dc.date.issued2021-08-13
dc.description.abstractOutside 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.en_US
dc.identifier.citationFarooqui, H. (2021). The Curry-Howard Correspondence (Master's thesis, University of Calgary, Calgary, Canada). Retrieved from https://prism.ucalgary.ca.en_US
dc.identifier.doihttp://dx.doi.org/10.11575/PRISM/39102
dc.identifier.urihttp://hdl.handle.net/1880/113742
dc.language.isoengen_US
dc.publisher.facultyArtsen_US
dc.publisher.institutionUniversity of Calgaryen
dc.rightsUniversity of Calgary graduate students retain copyright ownership and moral rights for their thesis. You may use this material in any way that is permitted by the Copyright Act or through licensing that has been assigned to the document. For uses that are not allowable under copyright legislation or licensing, you are required to seek permission.en_US
dc.subjectPhilosophyen_US
dc.subjectLogicen_US
dc.subjectUntyped Lambda Calculusen_US
dc.subjectSimply Typed Lambda Calculusen_US
dc.subjectCurry-Howarden_US
dc.subjectIsomorphismen_US
dc.subjectCorrespondenceen_US
dc.subjectProofs As Programsen_US
dc.subjectPropositions As Typesen_US
dc.subjectIntuitionistic Natural Deductionen_US
dc.subjectSequent Styleen_US
dc.subjectFormulae As Typesen_US
dc.subjectMetaphoren_US
dc.subject.classificationEducation--Mathematicsen_US
dc.subject.classificationPhilosophyen_US
dc.subject.classificationComputer Scienceen_US
dc.titleThe Curry-Howard Correspondenceen_US
dc.typemaster thesisen_US
thesis.degree.disciplinePhilosophyen_US
thesis.degree.grantorUniversity of Calgaryen_US
thesis.degree.nameMaster of Arts (MA)en_US
ucalgary.item.requestcopytrueen_US
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
ucalgary_2021_farooqui_husna.pdf
Size:
531.36 KB
Format:
Adobe Portable Document Format
Description:
Download
License bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
license.txt
Size:
2.62 KB
Format:
Item-specific license agreed upon to submission
Description:
Download
Collections
Open Theses and Dissertations