Logic Journal of IGPL Advance Access originally published online on October 12, 2007
Logic Journal of IGPL 2007 15(5-6):707-739; doi:10.1093/jigpal/jzm045
Fibred and Indexed Categories for Abstract Model Theory
Instituto de Informática – PUCRS – Brasil. E-mail: alfio{at}inf.pucrs.br
Institute of Informatics – University of Bergen – Norway. E-mail: wolter{at}ii.uib.no
Departamento de Ciência da Computação – PUC-Rio – Brasil. E-mail: hermann{at}inf.puc-rio.br
Indexed and Fibred category theory have a long tradition in computer science as a language to formalize different presentations of the notion of a logic, as for instance, in the theory of institutions and general logics, and as unifying models of (categorical) logic and type theory as well. Here we introduce the notions of indexed and fibred frames and construct a rich mathematical workspace where many relevant and useful concepts of logics can be elegantly modelled. To demonstrate the applicability of these tools, essential ideas around the theory of institutions are recasted and described.
Key Words: indexed and fibred categories • Grothendieck constructions • logical systems • institutions.
Received for publication 20 September 2006.
References
-
1 Arrais M, Fiadeiro JL. Unifying Theories in Different Institutions. In: Recent Trends in Data Type Specification (1996) 11th Workshop on Specification of Abstract Data Types. Springer, LNCS 1130. 81–101.
2 Bairwise KJ. Axioms for Abstract Model Theory. Annals of Mathematical Logic (1974) 7:221–265.[CrossRef]
3 Barr M, Wells C. Category Theory for Computing Science (1990) London: Series in Computer Science. Prentice Hall International.
4 Bénabou J. Fibred categories and the foundations of naive category theory. Journal of Symbolic Logic (1985) 50(1):10–37.[CrossRef][Web of Science]
5 Burstall RM, Goguen JA. Putting theories together to make specifications. In: Proc. Int. Conf. Artificial Intelligence (1977).
6 Burstall RM, Goguen JA. The semantics of Clear, a specification language. In: Abstract Software Specification, Proc. 1979 Copenhagen Winter School, LNCS 86—Bjøner D, ed. (1980) Springer. 292–332.
7 Cerioli M, Meseguer J. May i borrow your logic? (transporting logical structures along maps). Theoretical Computer Science (1997) 173(2):311–347.[CrossRef][Web of Science]
8 Diaconescu R. Extra-theory morphisms in institutions: logical semantics for multi-paradigm languages. In: Journal Applied Categorical Structures (1998).
9 Diaconescu R. Grothendieck Institutions. Applied Categorical Structures (2002) 10(4):383–402.[CrossRef][Web of Science]
10 Girard JY, Lafont Y, Taylor P. Proofs and Types (1989) Cambridge University Press.
11 Goguen JA, Burstall RM. Institutions: Abstract Model Theory for Specification and Programming. In: Journal of the ACM (1992) January;39(1):95–146.[CrossRef][Web of Science]
12 Goguen JA, Ro
u G. Institutions morphisms. Formal Aspects of Computing (2002) July;12(3–5):274–307.
13 Goldblatt R. Logics of Time and Computation (1992) 2nd ed. CSLI Lecture Notes No. 7: Centre for the Study of Language and Information, Stanford University. University of Chicago Press.
14 Haeusler EH, Martini A, Wolter U. Indexed General Logics. In: Logical and Semantical Frameworks, LSFA'06, September 17th, 2006, Natal, Brasil,Pre-proceedings—Hermann Haeusler E, Braga Christiano, Ayala Rincon Mauricio, eds. (2006).
15 Jacobs B. Categorical Logic and Type Theory (2001) Amsterdam: Elsevier. volume 141 of Studies in Logic and the Foundations of Mathematics.
16 Lawvere FW. Adjointness in foundations. In: Dialectica (1969) 281–296.
17 Lindstrom P. On extensions of elementary logic. In: Theoria, 35 (1969) 1–11.
18 Makkai M, Reyes GE. First order categorical logic. Lecture Notes in Mathematics (1977) 611:159–176.
19 Martini A. Relating Arrows between Institutions in a Categorical Framework. In: PhD thesis (1999) Technical University of Berlin.
20 Meseguer J. General logics. In: Logic colloquium '87—Ebbinghaus H-D, et al, eds. (1989) North Holland: Elsevier Science Publishers B. V. 275–329.
21 Moerdijk Ieke, Mac Lane Saunders. Sheaves in Geometry and Logic (1992) New York: Springer Berlag.
22 Mossakowski T. Comorphism-based Grothendieck logics. In: Mathematical Foundations of Computer Science 2002, Proceedings (2002) 27th International Symposium, MFCS 2002, August 26-30, 2002: Warsaw, Poland. Springer Verlag, LNCS 2420. 593–604.
23 Mossakowski T. Heterogeneous development graphs and heterogeneous borrowing. In: Foundations of Software Science and Computational Structures (2002) Springer: LNCS 2303. 326–341.
24 Mossakowski T. Foundations of Heterogeneous Specification. In: Recent Trends in Algebraic Development Techniques, 16th International Workshop, WADT 2002, Frauenchiemsee, Germany, September 24-27, 2002, Revised Selected Papers—Wirsing M, Pattinson D, Hennicker R, eds. (2003) Springer Verlag: LNCS 2755. 359–375.
25 Blackburn P, van Benthem J. Handbook of Modal Logic (2006) Elsevier. chapter Modal Logic: A Semantic Perspective.
26 Pitts AM. Categorical logic. In: Handbook of Logic in Computer Science, Volume 5. Algebraic and Logical Structures—Abramsky S, Gabbay DM, Maibaum TSE, eds. (2000) Oxford University Press. 39–128.
27 Tarlecki A, Burstall RM, Goguen JA. Some fundamental algebraic tools for the semantics of computation. Part III: Indexed categories. TCS (1991) 91:239–264.[CrossRef]
28 Wolter U, Didrich K, Cornelius F, Klar M, Wessäly R, Ehrig H. How to Cope with the Spectrum of Spectrum. Technical Report Bericht-Nr. (1994) TU Berlin: FB Informatik. 94–22.
29 Wolter U, Klar M, Wessäly R, Cornelius F. Four Institutions — A Unified Presentation of Logical Systems for Specification. In: Technical Report Bericht-Nr (1994) TU Berlin: Fachbereich Informatik. 94–24.
CiteULike 
Connotea 
Del.icio.us What's this?
| ||||||||||||||||||||||||||||||||||||||||||||||||||