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

 

 

more>>  
Visitor:3140793
Top Paper  |  E-mail Alert  |  Publication Ethics  |  New Version

© Copyright by Institute of Software, the Chinese Academy of Sciences
京ICP备05046678号-5

京公网安备 11040202500065号