An Institutional View on Categorical Logic.
Joseph A. Goguen, Till Mossakowski, Valeria de Paiva, Florian Rabe, Lutz Schröder · 2007
We introduce a generic notion of categorical propositional logic and provide a construction of a preorder-enriched institution out of such a logic, following the Curry-Howard-Tait paradigm. The logics are specified as theories of a meta-logic within the logical framework LF such that institution comorphisms are obtained from theory morphisms of the metalogic. We prove several logic-independent results including soundness and completeness theorems and instantiate our framework with a number of examples: classical, intuitionistic, linear and modal propositional logic.