An Institutional View on Categorical Logic (bibtex)

by Joseph Goguen, Till Mossakowski, Valeria De Paiva, Florian Rabe and Lutz Schröder

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.

Reference:

Joseph Goguen, Till Mossakowski, Valeria De Paiva, Florian Rabe and Lutz Schröder: An Institutional View on Categorical Logic, In Int J Software Informatics, vol. 1(1), pp. 129–152, 2007. [preprint]

Bibtex Entry:

@InProceedings{MossakowskiEA06a,
  author = {Joseph Goguen and Till Mossakowski and Valeria De Paiva and Florian Rabe and Lutz Schr{\"o}der},
  title = {An Institutional View on Categorical Logic},
  year = {2007},
  booktitle = {Int J Software Informatics},
  volume = {1},
  pages = {129-152},
  number = {1},
  comment = { <a href = "http://www.informatik.uni-bremen.de/~till/papers/CurryHoward.pdf"> [preprint] </a>},
  psurl = {http://www.informatik.uni-bremen.de/~till/papers/CurryHoward.ps},
  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.},
  status = {Other}
}