Cartesian Closed Categories and Typed Lambda Calculi

Access full-text files

Date

2016

Authors

Menezes, Dean

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Typed lambda categories and Cartesian closed categories are both means of formalizing the process of substitution; we demonstrate that these views are essentially the same; specifically that there is an equivalence between the category of small Cartesian closed categories and the category of typed lambda calculi. First we introduce the basic notions of category, functor, monad, comonad and equivalence of categories; then we use these notions to define the category of small Cartesian closed categories and describe how additional arrows may be adjoined to a Cartesian closed category. Next we provide a definition of a typed lambda calculus and describe the structure-preserving maps or translations between typed lambda calculi. Next we provide a definition of a typed lambda calculus and describe the structure-preserving maps or translations between typed lambda calculi. Having defined the two categories we provide descriptions of functors L : Cart_N to lambda-calc and C: lambda-calc to Cart_N and then show that the functors give an equivalence of categories.

Department

Description

LCSH Subject Headings

Citation

Collections