Showing 1–1 of 1 results for author: Meleiro, J F

Formalizing the Curry-Howard Correspondence

Authors: Juan Ferrer Meleiro, Hugo Luiz Mariano

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 corresp… ▽ More 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 $λ$-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. △ Less

Submitted 23 December, 2019; originally announced December 2019.

Comments: 26 pages. For the full source, see https://gitlab.com/juanmeleiro/ic.git or contact Juan Meleiro