[For the entire collection see Zbl 0599.00011.]
Many different languages have been proposed for specification, verification, and design in computer science; moreover, these languages are based upon many different logical systems. In an attempt to comprehend this density, the theory of institutions formalizes the intuitive notion of a ”logical system”. A number of general linguistic features have been defined ”institutionally” and are thus available for any language based upon a suitable institution. These features include generic modules, module hierarchies, ”data constraints” (for data abstraction), and multiplex institutions (for combining multiple logical systems). In addition, institution morphisms support the transfer of results (as well as associated artifacts, such as theorem provers) from one language to another. More generally, institutions are intended to support as much computer science as possible independently of the underlying logical system.
This viewpoint extends from specification languages to programming languages, where, in addition to the programming-in-the-large features mentioned above, it provides a precise basis for a ”wide spectrum” integration of programming and specification. A logical programming language is one whose statements are sentences in an institution, whose operational semantics is based upon deduction in that institution, and whose mathematical semantics are given by an initial model in that institution, giving a ”closed world” for a program. This notion encompasses a number of modern programming paradigms, including functional, logic, and object-oriented, and has been useful in unifying these paradigms, by unifying their underlying institutions, as well as in providing them with sophisticated facilities for data abstraction and programming-in-the-large.