CafeOBJ Traces

  • Răzvan Diaconescu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)


We survey two important distinctive features of CafeOBJ, namely behavioural specification based upon coherent hidden algebra and heterogeneous specification based upon Grothendieck institutions. Both of them represent seminal contributions to formal specification culture that go much beyond the realm of CafeOBJ. Our presentation includes rather detailed explanations of the motivations and of the process leading to the inception of these concepts and theories. The paper is dedicated to Professor Kokichi Futatsugi, the leader of the CafeOBJ project, and also close friend and collaborator, on the occasion of his retirement.


Natural Transformation Institution Theory Logic Combination Model Amalgamation Signature Morphism 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Béziau, J.-Y.: 13 questions about universal logic. Bulletin of the Section of Logic 35(2/3), 133–150 (2006)MathSciNetzbMATHGoogle Scholar
  3. 3.
    Burstall, R., Diaconescu, R.: Hiding and behaviour: An institutional approach. In: William Roscoe, A. (ed.) A Classical Mind: Essays in Honour of C.A.R. Hoare, pp. 75–92. Prentice-Hall, 1994. Also in Technical Report ECS-LFCS-8892-253, Laboratory for Foundations of Computer Science, University of Edinburgh (1992)Google Scholar
  4. 4.
    Carnielli, W., Coniglio, M., Gabbay, D.M., Gouveia, P., Sernadas, C.: Analysis and Synthesis of Logics How to Cut and Paste Reasoning Systems. Applied Logic —Series, vol. 35. Springer (2008)Google Scholar
  5. 5.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)zbMATHGoogle Scholar
  6. 6.
    Diaconescu, R.: Behavioural coherence in object-oriented algebraic specification. Technical Report IS-RR-98-0017F, Japan Advanced Institute for Science and Technology (June 1998)Google Scholar
  7. 7.
    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 1997Google Scholar
  8. 8.
    Diaconescu, R.: Grothendieck institutions. Applied Categorical Structures 10(4), 383–402 (2002); Preliminary version appeared as IMAR Preprint 2-2000 (February 2000) ISSN 250-3638Google Scholar
  9. 9.
    Diaconescu, R.: Interpolation in Grothendieck institutions. Theoretical Computer Science 311, 439–461 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Diaconescu, R.: Behavioural specification of hierarchical object composition. Theoretical Computer Science 343(3), 305–331 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Diaconescu, R.: Institution-independent Model Theory. Birkhäuser (2008)Google Scholar
  12. 12.
    Diaconescu, R.: Coinduction for preordered algebras. Information and Computation 209(2), 108–117 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Diaconescu, R.: Grothendieck inclusion systems. Applied Categorical Structures 19(5), 783–802 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Diaconescu, R.: Quasi-varieties and initial semantics in hybridized institutions. Journal of Logic and Computation, doi:10.1093/logcom/ext016Google Scholar
  15. 15.
    Diaconescu, R., Ţuţu, I.: Foundations for structuring behavioural specifications. Journal of Logic and Algebraic Programming (to appear)Google Scholar
  16. 16.
    Diaconescu, R., Ţuţu, I.: On the algebra of structured specifications. Theoretical Computer Science 412(28), 3145–3174 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Diaconescu, R., Futatsugi, K.: CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification. AMAST Series in Computing, vol. 6. World Scientific (1998)Google Scholar
  18. 18.
    Diaconescu, R., Futatsugi, K.: Behavioural coherence in object-oriented algebraic specification. Universal Computer Science 6(1), 74–96 (2000); First version appeared as JAIST Technical Report IS-RR-98-0017F (June 1998)Google Scholar
  19. 19.
    Diaconescu, R., Futatsugi, K.: Logical foundations of CafeOBJ. Theoretical Computer Science 285, 289–318 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Diaconescu, R., Goguen, J., Stefaneas, P.: Logical support for modularisation. In: Huet, G., Plotkin, G. (eds.) Logical Environments, pp. 83–130. Cambridge (1993). Proceedings of a Workshop held in Edinburgh, Scotland (May 1991)Google Scholar
  21. 21.
    Diaconescu, R., Stefaneas, P.: Ultraproducts and possible worlds semantics in institutions. Theoretical Computer Science 379(1), 210–230 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Finger, M., Gabbay, D.M.: Adding a temporal dimension to a logic system. Journal of Logic, Language and Information 1(3), 203–233 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Goguen, J.: Types as theories. In: Reed, G.M., Roscoe, A.W., Wachter, R.F. (eds.) Topology and Category Theory in Computer Science, pp. 357–390. Oxford (1991). Proceedings of a Conference held at Oxford (June 1989)Google Scholar
  24. 24.
    Goguen, J.: Data, schema, ontology and logic integration. Journal of IGPL 13(6), 685–715 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Goguen, J., Burstall, R.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39(1), 95–146 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    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)CrossRefGoogle Scholar
  27. 27.
    Goguen, J., Roşu, G.: Institution morphisms. Formal Aspects of Computing 13, 274–307 (2002)CrossRefzbMATHGoogle Scholar
  28. 28.
    Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. In: Goguen, J., Malcolm, G. (eds.) Software Engineering with OBJ: Algebraic Specification in Action. Kluwer (2000)Google Scholar
  29. 29.
    Grothendieck, A.: Catégories fibrées et descente. In: Revêtements Étales et Groupe Fondamental, Séminaire de Géométrie Algébraique du Bois-Marie 1960/61, Exposé VI. Lecture Notes in Mathematics, vol. 224. Institut des Hautes Études Scientifiques (1963); Reprinted in Lecture Notes in Mathematics, vol. 224, pp. 145–194. Springer (1971)Google Scholar
  30. 30.
    Iida, S.: An Algebraic Formal Method for Component based Software Developments. PhD thesis, Japan Advanced Institute for Science and Technology (1999)Google Scholar
  31. 31.
    Jacobs, B., Rutten, J.M.: A tutorial on (co)algebras and (co)induction. Bulletin of EATCS 62, 222–259 (1997)zbMATHGoogle Scholar
  32. 32.
    Martins, M.A., Madeira, A., Diaconescu, R., Barbosa, L.S.: Hybridization of institutions. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 283–297. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  33. 33.
    Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  34. 34.
    Mossakowski, T.: Comorphism-based Grothendieck logics. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 593–604. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  35. 35.
    Mossakowski, T., Kutz, O., Lange, C.: Semantics of Distributed Ontology Language: Institutes and institutions. In: Martí-Oliet, N., Palomino, M. (eds.) WADT 2012. LNCS, vol. 7841, pp. 212–230. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  36. 36.
    Popescu, A., Roşu, G.: Behavioral extensions of institutions. In: Fiadeiro, J.L., Harman, N.A., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol. 3629, pp. 331–347. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  37. 37.
    Reichel, H.: Behavioural equivalence – a unifying concept for initial and final specifications. In: Proceedings, Third Hungarian Computer Science Conference, Akademiai Kiado, Budapest (1981)Google Scholar
  38. 38.
    Roşu, G.: Hidden Logic. PhD thesis, University of California at San Diego (2000)Google Scholar
  39. 39.
    Roşu, G., Lucanu, D.: Circular coinduction: A proof theoretical foundation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 127–144. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  40. 40.
    Sannella, D., Tarlecki, A.: Foundations of Algebraic Specifications and Formal Software Development. Springer (2012)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Răzvan Diaconescu
    • 1
  1. 1.Simion Stoilow Institute of Mathematics Romanian AcademyRomania

Personalised recommendations