Formalizing the Curry-Howard Correspondence

TL;DR

This paper introduces p-institutions to unify various formulations of the Curry-Howard Correspondence, providing a more general framework and demonstrating its potential in theorem-proving environments like Idris.

Contribution

It formalizes the Curry-Howard Correspondence within the novel p-institutions framework, enabling more structured generalizations and linking it to practical theorem-proving tools.

Findings

Unified formalism for Curry-Howard using p-institutions

Restatement of the correspondence within the new formalism

Initial formalization in Idris demonstrating practical application

Abstract

The Curry-Howard Correspondence has a long history, and still is a topic of active research. Though there are extensive investigations into the subject, there doesn't seem to be a definitive formulation of this result in the level of generality that it deserves. In the current work, we introduce the formalism of p-institutions that could unify previous aproaches. We restate the tradicional correspondence between typed $\lambda$-calculi and propositional logics inside this formalism, and indicate possible directions in which it could foster new and more structured generalizations. Furthermore, we indicate part of a formalization of the subject in the programming-language Idris, as a demonstration of how such theorem-proving enviroments could serve mathematical research.