Skip to main content Skip to main navigation


An Institutional View on Categorical Logic

Joseph Goguen; Till Mossakowski; Valeria De Paiva; Florian Rabe; Lutz Schröder
In: International Journal of Software and Informatics (IJSI), Vol. 1, No. 1, Pages 129-152, 2007.


We introduce a generic notion of propositional categorical logic and provide a construction of an institution with proofs out of such a logic, following the Curry-Howard-Tait paradigm. We then prove logic-independent soundness and completeness theorems. The framework is instantiated with a number of examples: classical, intuitionistic, linear and modal propositional logics. Finally, we speculate how this framework may be extended beyond the propositional case.

Weitere Links