Artikel
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) Int J Software Informatics. Vol. 1, No. 1, Pages 129-152, o.A. 2007.
Abstract
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
http://www.informatik.uni-bremen.de/~till/papers/CurryHoward.pdf
http://www.informatik.uni-bremen.de/~till/papers/CurryHoward.ps