2016/12/08 by Schoenbaum, Lucius
#Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1612.02816
We present a variant of the calculus of deductive systems developed in (Lambek 1972, 1974), and give a generalization of the Curry-Howard-Lambek theorem giving an equivalence between the category of typed lambda-calculi and the category of cartesian closed categories and exponential-preserving morphisms that leverages the theory of generalized categories (Schoenbaum 2016). We discuss potential applications and extensions.