Introducing institutions. (English) Zbl 0543.68021

Logics of programs, Workshop, Pittsburgh/PA 1983, Lect. Notes Comput. Sci. 164, 221-256 (1984).
[For the entire collection see Zbl 0533.00026.]
This paper formalizes the intuitive notion of a logical system with the category-theoretic notion of an institution, which is intended to give a rich and flexible framework for program specification and other areas of theoretical computer science. Concerning this nobel notion, the authors establish the following results: (1) If an institution is such that interface declarations expressed in it can be glued togetheer, then theories in that institution can be glued together; (2) A suitable institution morphism permits a theorem prover for one institution to be used on theories from another; (3) Any institution supporting free constructions extends to another institution whose sentences may be either the old sentences, or else any of several kinds of constraint on interpretations.
Reviewer: H.Nishimura


68Q65 Abstract data types; algebraic specification
03G30 Categorical logic, topoi
03C95 Abstract model theory


Zbl 0533.00026