  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.
