## INSTITUTIONS: Abstract Model Theory for Specification and
Programming

**Joseph A Goguen and Rod Burstall**
*Abstract:* There is a population explosion among the
logical systems used in computer science. Examples include first
order logic, equational logic, Horn clause logic, higher order
logic, infinitary logic, dynamic logic, intuitionistic logic,
order-sorted logic, and temporal logic; moreover, there is a
tendency for each theorem prover to have its own ideosyncratic
``logical system''. The major requirement is that there is a
satisfaction relation between models and sentences which is
consistent under change of notation. Institutions enable us to
abstract from syntactic and semantic detail when working on
language structure ``in-the-large''; for example, we can define
language features for building large structures from smaller ones,
possibly involving parameters, without commitment to any particular
logical system. This applies to both specification languages and
programming languages. Institutions also have applications to such
areas as database theory and the semantics of artificial and
natural languages. A first main result of this paper says that any
institution such that signatures (which define notation) can be
glued together, also allows gluing together theories (which are
just collections of sentences over a fixed signature). A second
main result considers when theory structuring is preserved by
institution morphisms. A third main result gives conditions under
which it is sound to use a theorem prover for one institution on
theories from another. A fourth main result shows how to extend
institutions so that their theories may include, in addition to the
original sentences, various kinds of constraint that are useful for
defining abstract data types, including both ``data'' and
``hierarchy'' constraints. Further results show how to define
institutions that allow sentences and constraints from two or more
institutions. All our general results apply to such ``duplex'' or
``multiplex'' institutions.

*LFCS report ECS-LFCS-90-106*

Previous |

Index |

Next