Institution (computer science)

The notion of institution was created by Joseph Goguen and Rod Burstall in the late 1970s, in order to deal with the "population explosion among the logical systems used in computer science". The notion attempts to "formalize the informal" concept of logical system.[1]

The use of institutions makes it possible to develop concepts of specification languages (like structuring of specifications, parameterization, implementation, refinement, and development), proof calculi, and even tools in a way completely independent of the underlying logical system. There are also morphisms that allow to relate and translate logical systems. Important applications of this are re-use of logical structure (also called borrowing), and heterogeneous specification and combination of logics.

The spread of institutional model theory has generalized various notions and results of model theory, and institutions themselves have impacted the progress of universal logic.[2][3]

  1. ^ J. A. Goguen; R. M. Burstall (1992), "Institutions: Abstract model theory for specification and programming", Journal of the ACM, 39 (1): 95–146, doi:10.1145/147508.147524, S2CID 16856895
  2. ^ Razvan Diaconescu (2012), "Three decades of institution theory", in Jean-Yves Béziau (ed.), Universal Logic: An Anthology, Springer, pp. 309–322
  3. ^ T. Mossakowski; J. A. Goguen; R. Diaconescu; A. Tarlecki (2007), "What is a logic?: In memoriam Joseph Goguen", in Jean-Yves Beziau (ed.), Logica Universalis: Towards a General Theory of Logic (2nd ed.), Birkhäuser, Basel, pp. 113–133, doi:10.1007/978-3-7643-8354-1_7