Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Jewels of Institution-Independent Model Theory

  • Chapter
Algebra, Meaning, and Computation

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4060))

Abstract

This paper is dedicated to Joseph Goguen, my beloved teacher and friend, on the ocassion of his 65th anniversary. It is a survey of institution-independent model theory as it stands today, the true form of abstract model theory which is based on the concept of institution. Institution theory was co-fathered by Joseph Goguen and Rod Burstall in late 1970’s. In the final part we discuss some philosophical roots of institution-independent methodologies.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andréka, H., Németi, I.: A general axiomatizability theorem formulated in terms of cone-injective subcategories. In: Csakany, B., Fried, E., Schmidt, E.T. (eds.) Universal Algebra. Colloquia Mathematics Societas János Bolyai, vol. 29, pp. 13–35. North-Holland, Amsterdam (1981)

    Google Scholar 

  2. Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P., Sannella, D., Tarlecki, A.: CASL: The common algebraic specification language. Theoretical Computer Science 286(2), 153–196 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  3. Barbier, F.: Géneralisation et préservation au travers de la combinaison des logique des résultats de théorie des modèles standards liés à la structuration des spécifications algébriques. PhD thesis, Université Evry (2005)

    Google Scholar 

  4. Barwise, J.: Axioms for abstract model theory. Annals of Mathematical Logic 7, 221–265 (1974)

    Article  MATH  MathSciNet  Google Scholar 

  5. Barwise, J., Feferman, S.: Model-Theoretic Logics. Springer, Heidelberg (1985)

    Google Scholar 

  6. Bernot, G., Le Gall, P., Aiguier, M.: Label algebras and exception handling. Science of Computer and Programming 23, 227–286 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  7. Bidoit, M., Hennicker, R.: On the integration of the observability and reachability concepts. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 21–36. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Borzyszkowski, T.: Higher-order logic and theorem proving for structured specifications. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 401–418. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  9. Borzyszkowski, T.: Logical systems for structured specifications. Theoretical Computer Science 286(2), 197–245 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  10. Burmeister, P.: A Model Theoretic Oriented Approach to Partial Algebras. Akademie-Verlag, Berlin (1986)

    MATH  Google Scholar 

  11. Burstall, R., Goguen, J.: Semantics of Clear. In: Unpublished notes handed out at the 1978 Symposium on Algebra and Applications, Stefan Banach Center, Warsaw (1978)

    Google Scholar 

  12. Chang, C.C., Keisler, H.J.: Model Theory. North Holland, Amsterdam (1990)

    MATH  Google Scholar 

  13. Círstea, C.: Institutionalising many-sorted coalgebraic modal logic. In Coalgebraic Methods in Computer Science 2002, Electronic Notes in Theoretical Computer Science (2002)

    Google Scholar 

  14. Sȩrbănut¸ă, T.: Institutional concepts in first-order logic, parameterized specification, and logic programming. Master’s thesis, University of Bucharest (2004)

    Google Scholar 

  15. Căzănescu, V.E., Ros̨u, G.: Weak inclusion systems. Mathematical Structures in Computer Science 7(2), 195–206 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  16. Diaconescu, R.: Institution-independent Model Theory. Book draft (Ask author for current draft at Razvan.Diaconescu@imar.ro) (to appear)

    Google Scholar 

  17. Diaconescu, R.: Extra theory morphisms for institutions: logical semantics for multi-paradigm languages. Applied Categorical Structures 6(4), 427–453 (1998), A preliminary version appeared as JAIST Technical Report IS-RR-97-0032F in 1997

    Article  MATH  MathSciNet  Google Scholar 

  18. Diaconescu, R.: Grothendieck institutions. Applied Categorical Structures 10(4), 383–402 (2002), Preliminary version appeared as IMAR Preprint 2-2000, ISSN 250-3638 (February 2000)

    Article  MATH  MathSciNet  Google Scholar 

  19. Diaconescu, R.: Institution-independent ultraproducts. Fundamenta Informaticæ 55(3-4), 321–348 (2003)

    MATH  MathSciNet  Google Scholar 

  20. Diaconescu, R.: Elementary diagrams in institutions. Journal of Logic and Computation 14(5), 651–674 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  21. Diaconescu, R.: Herbrand theorems in arbitrary institutions. Information Processing Letters 90, 29–37 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  22. Diaconescu, R.: An institution-independent proof of Craig Interpolation Theorem. Studia Logica 77(1), 59–79 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  23. Diaconescu, R.: Interpolation in Grothendieck institutions. Theoretical Computer Science 311, 439–461 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  24. Diaconescu, R.: Proof systems for institutional logic. Journal of Logic and Computation (2006) (to appear)

    Google Scholar 

  25. Diaconescu, R., Futatsugi, K.: Logical foundations of CafeOBJ. Theoretical Computer Science 285, 289–318 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  26. Diaconescu, R., Goguen, J., Stefaneas, P.: Logical support for modularisation. In: Huet, G., Plotkin, G. (eds.) Proceedings of a Workshop held in Logical Environment, Edinburgh, Scotland (May 1991)

    Google Scholar 

  27. Diaconescu, R., Petria, M.: Saturated models in institutions. (in preparation)

    Google Scholar 

  28. Diaconescu, R., Stefaneas, P.: Possible worlds semantics in arbitrary institutions. Technical Report 7, Institute ofMathematics of the Romanian Academy, ISSN 250-3638 (June 2003)

    Google Scholar 

  29. Dimitrakos, T., Maibaum, T.: On a generalized modularization theorem. Information Processing Letters 74, 65–71 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  30. Fiadeiro, J.L., Costa, J.F.: Mirror, mirror in my hand: A duality between specifications and models of process behaviour. Mathematical Structures in Computer Science 6(4), 353–373 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  31. Goguen, J., Burstall, R.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39(1), 95–146 (1992)

    MATH  MathSciNet  Google Scholar 

  32. Goguen, J., Diaconescu, R.: Towards an algebraic semantics for the object paradigm. In: Ehrig, H., Orejas, F. (eds.) Abstract Data Types 1992 and COMPASS 1992. LNCS, vol. 785, pp. 1–34. Springer, Heidelberg (1994)

    Google Scholar 

  33. Grätzer, G.: Universal Algebra. Springer, Heidelberg (1979)

    MATH  Google Scholar 

  34. G˘ain˘a, D., Popescu, A.: An institution-independent generalization of Tarski’s Elementary Chain Theorem. Journal of Logic and Computation (to appear)

    Google Scholar 

  35. G˘ain˘a, D., Popescu, A.: An institution-independent proof of Robinson consistency theorem. Studia Logica (to appear)

    Google Scholar 

  36. Bell, J.L., Slomson, A.B.: Models and Ultraproducts. North-Holland, Amsterdam (1969)

    MATH  Google Scholar 

  37. Lambek, J., Scott, P.: Introduction to Higher Order Categorical Logic, Cambridge. Cambridge Studies in Advanced Mathematics, vol. 7 (1986)

    Google Scholar 

  38. Lane, S.M.: Categories for the Working Mathematician, 2nd edn. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  39. Łoś, J.: Quleques remarques, théorèmes et problèmes sur les classes définissables d’algèbres. In: Mathematical Interpretation of Formal Systems, pp. 98–113. North-Holland, Amsterdam (1955)

    Google Scholar 

  40. Makkai, M.: Ultraproducts and categorical logic. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 222–309. Springer, Heidelberg (1996)

    Google Scholar 

  41. Makkai Stone, M.: duality for first order logic. Advances in Mathematics 65(2), 97–170 (1987)

    Article  MathSciNet  Google Scholar 

  42. Malcev, I.: The Metamathematics of Algebraic Systems. North-Holland, Amsterdam (1971)

    Google Scholar 

  43. Matthiessen, G.: Regular and strongly finitary structures over strongly algebroidal categories. Canad. J. Math. 30, 250–261 (1978)

    Article  MATH  MathSciNet  Google Scholar 

  44. Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  45. Meseguer, J.: A logical theory of concurrent objects and its realization in the Maude language. In: Agha, G., Wegner, P., Yonezawa, A. (eds.) Research Directions in Concurrent Object-Oriented Programming, The MIT Press, Cambridge (1993)

    Google Scholar 

  46. Mossakowski, T.: Comorphism-based Grothendieck logics. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 593–604. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  47. Mossakowski, T.: Foundations of heterogeneous specification. In: 16th Workshop on Algebraic Development Techniques 2002. LNCS, Springer, Heidelberg (2003)

    Google Scholar 

  48. Mossakowski, T., Goguen, J., Diaconescu, R., Tarlecki, A.: What is a logic. In: Beziau, J.-Y. (ed.) Logica Universalis, pp. 113–133. Birkhauser, Basel (2005)

    Chapter  Google Scholar 

  49. Petria, M., Diaconescu, R.: Abstract Beth definability in institutions. Journal of Symbolic Logic (2006) (to appear)

    Google Scholar 

  50. Popescu, A., Sęrbănut̨ă, T., Ros̨u, G.: A semantic approach to interpolation (submitted)

    Google Scholar 

  51. Salibra, A., Scollo, G.: Interpolation and compactness in categories of pre-institutions. Mathematical Structures in Computer Science 6, 261–286 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  52. Schröder, L., Mossakowski, T., Lüth, C.: Type class polymorphism in an institutional framework. In: Fiadeiro, J.L., Mosses, P.D., Orejas, F. (eds.) WADT 2004. LNCS, vol. 3423, pp. 234–248. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  53. Tarlecki, A.: Bits and pieces of the theory of institutions. In: Poigné, A., Pitt, D.H., Rydeheard, D.E., Abramsky, S. (eds.) Category Theory and Computer Programming. LNCS, vol. 240, pp. 334–360. Springer, Heidelberg (1986)

    Google Scholar 

  54. Tarlecki, A.: On the existence of free models in abstract algebraic institutions. Theoretical Computer Science 37, 269–304 (1986), Preliminary version, University of Edinburgh, Computer Science Department, Report CSR-165-84 (1984)

    Article  MathSciNet  Google Scholar 

  55. Tarlecki, A.: Quasi-varieties in abstract algebraic institutions. Journal of Computer and System Sciences 33(3), 333–360 (1986), Original version, University of Edinburgh, Report CSR-173-84.

    Article  MATH  MathSciNet  Google Scholar 

  56. Tarlecki, A., Burstall, R., Goguen, J.: Some fundamental algebraic tools for the semantics of computation, part 3: Indexed categories. Theoretical Computer Science 91, 239–264 (1991), Also, Monograph PRG–77, Programming Research Group, Oxford University (August 1989)

    Article  MATH  MathSciNet  Google Scholar 

  57. Tarski, A., Vaught, R.: Arithmetical extensions of relational systems. Compositio Mathematicæ 13, 81–102 (1957)

    MathSciNet  Google Scholar 

  58. His Holiness the XIVth Dalai Lama. The Universe in a Single Atom. Wisdom Publications (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Mathematics of the Romanian Academy,  

    Răzvan Diaconescu

Authors
  1. Răzvan Diaconescu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Japan Advanced Institute of Science and Technology (JAIST),  

    Kokichi Futatsugi

  2. LIX, Projet INRIA TypiCal, École Polytechnique and CNRS, 91400, Palaiseau, France

    Jean-Pierre Jouannaud

  3. CS Dept., University of Illinois at Urbana-Champaign, USA

    José Meseguer

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Diaconescu, R. (2006). Jewels of Institution-Independent Model Theory. In: Futatsugi, K., Jouannaud, JP., Meseguer, J. (eds) Algebra, Meaning, and Computation. Lecture Notes in Computer Science, vol 4060. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11780274_5

Download citation

  • DOI: https://doi.org/10.1007/11780274_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-35462-8

  • Online ISBN: 978-3-540-35464-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation