A Generalization of the Curry-Howard Correspondence

TL;DR

This paper generalizes the Curry-Howard correspondence by introducing a variant of Lambek's calculus and establishing an equivalence with cartesian closed categories using generalized categories, expanding theoretical understanding.

Contribution

It extends the Curry-Howard-Lambek theorem to a broader setting through the use of generalized categories, connecting typed lambda-calculi with categorical structures.

Findings

Establishes an equivalence between typed lambda-calculi and cartesian closed categories.

Introduces a variant of Lambek's calculus for this generalization.

Discusses potential applications and extensions of the generalized correspondence.

Abstract

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.