A Categorical Extension of the Curry-Howard Isomorphism
Date
2019-09
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Within this work, we investigate some aspects of the interaction that occurs between category theory and the typed λ-calculus. In particular, we examine the equivalence of categories that can be demonstrated between the category of Cartesian closed categories and the category of typed λ-theories. As will be seen, a convenient technique that can be employed so as to make this interaction explicit is the application of algebraic theories (often known as “Lawvere theories”), which allow us to characterize various model-theoretical aspects of typed λ-theories in the abstract algebraic setting of a Cartesian closed category. What follows from this interaction between Cartesian closed categories and typed λ-theories is that of a categorical extension of the Curry-Howard isomorphism, which attributes a similar correspondence between the typed λ-calculus and the positive fragment of the intuitionistic propositional calculus.
Description
Keywords
Category Theory, Logic
Citation
McDonald, J. (2019). A Categorical Extension of the Curry-Howard Isomorphism (Master's thesis, University of Calgary, Calgary, Canada). Retrieved from https://prism.ucalgary.ca.