The paper introduces a notion of a context institution. The notion is explicitly illustrated by two standard examples. Morphism between context institutions are introduced, thus yielding a category of context institutions. Some expected constructions on context institutions are presented as functors from this category. The potential usefulness of these notions is illustrated by one such a construction, yielding a Hoare logic for an arbitrary small context institution satisfying mild extra assumptions.


Context Institution Natural Transformation Satisfaction Condition Coherence Condition Satisfaction Relation 
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.
    K.R. Apt. Ten years of Hoare logic: A survey—Part 1. ACM Transactions on Programming Languages and Systems Vol. 3, No. 4, pp. 431–483, 1981.Google Scholar
  2. 2.
    M. Bidoit and A. Tarlecki. Behavioral satisfaction and equivalence in concrete model categories. Technical report, full version.Google Scholar
  3. 3.
    R. Diaconescu, J. Goguen, and P. Stefaneas. Logical Support for Modularisation. In G. Huet and G. Plotkin, editors, Logical Environments, pp. 83–130, Cambridge University Press, 1993.Google Scholar
  4. 4.
    J. Goguen and R. Burstall. Introducing Institutions. In Proceedings, Logics of Programming Workshop, LNCS 164, pp. 221–256, Springer-Verlag, 1984.Google Scholar
  5. 5.
    J. Goguen and R. Burstall. A study in the foundations of programming methodology: Specifications, institutions, charters and parchments. In D. Pitt, S. Abramsky, A Poigné, and D. Rydeheard, editors, Proceedings, Conference on Category Theory and Computer Programming, LNCS 240, pp. 313–333, Springer-Verlag, 1986.Google Scholar
  6. 6.
    J. Goguen and R. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 39(1), pp. 95–146, January 1992.Google Scholar
  7. 7.
    R. Harper, D. Sannella, and A. Tarlecki. Logic Representation in LF. In D.H. Pitt, D.E. Rydeheard, P. Dybjer, A.M. Pitts, and A. Poigné, editors, Proceedings, Conference on Category Theory and Computer Science, Manchester 1989, LNCS 389, pp. 250–272, Springer-Verlag, 1989.Google Scholar
  8. 8.
    H. Herrlich and G.E. Strecker. Category Theory. Allyn and Bacon Inc, Boston, 1973.Google Scholar
  9. 9.
    T. Mossakowski. Using Limits of Parchments to Systematically Construct Institutions of Partial Algebras. Recent Trends in Data Type Specifications, 11th Workshop on Specification of Abstract Data Types, WADT11. Oslo Norway, September 1995, Springer LNCS, this volume, pp. 362–376, Springer-Verlag 1996.Google Scholar
  10. 10.
    A. Tarlecki. Bits and pieces of the theory of institutions. In D. Pitt, S. Abramsky, A Poigné, and D. Rydeheard, editors, Proceedings, Conference on Category Theory and Computer Programming, LNCS 240, pp. 334–360, Springer-Verlag, 1986.Google Scholar
  11. 11.
    A. Tarlecki, R. Burstall, and J. Goguen. Some fundamental algebraic tools for the semantics of computation, part 3: Indexed categories. Theoretical Computer Science, 91, pp. 239–264, 1991.Google Scholar
  12. 12.
    U. Wolter, R. Wessäly, M. Klar, and F. Cornelius. Four Institutions: A Unified Presentation of Logical Systems for Specification. Bericht-Nr. 94-24, Technische Universität Berlin, 1994.Google Scholar
  13. 13.
    E. Zucca. Building institutions of dynamic data-types. Talk presented during FLIRTS'95 Workshop, Genova, 26–28 October 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Wiesław Pawłowski
    • 1
  1. 1.Institute of Computer SciencePolish Academy of SciencesSopotPoland

Personalised recommendations