A Categorical Extension of the Curry-Howard Isomorphism

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.