Introducing institutions. (English) Zbl 0543.68021

Goguen, J. A.; Burstall, R. M.

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

MSC:

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

Keywords:

logical system; institution; program specification; interface declarations; theories; theorem prover; free constructions

Citations:

Zbl 0533.00026