An Institutional View on Categorical Logic |
Received:October 01, 2007 Revised:December 16, 2007 Download PDF |
Joseph Goguen,Till Mossakowski,Valeria de Paiva,Florian Rabe,Lutz Schr?der. An Institutional View on Categorical Logic. International Journal of Software and Informatics, 2007,1(1):129~152 |
Hits: 3996 |
Download times: 3047 |
Joseph Goguen Till Mossakowski Valeria de Paiva Florian Rabe Lutz Schr?der |
|
|
Abstract: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 speci ed as theories of a meta-logic within the logical
framework LF such that institution comorphisms are obtained from theory morphisms of the meta-logic. 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. |
keywords:categorical logic propositional logic institutions logic translations Curry-Howard-Tait isomorphism |
View Full Text View/Add Comment Download reader |