# Institutions

**Institutions**, introduced by Goguen and Burstall in the
eighties, are abstract model-theoretic notions of logical systems. Most logics in current use are particular cases of institutions. This qualifies the theory of institutions as a framework for proving properties about *logical systems, in general*. This is particularly appropriate in the world of algebraic specifications, where a large variety of logics is used. In order to see the forest beyond the trees, one can state and discuss many desirable properties at the abstract level of institutions, and then apply the results to any particular logic.

Our work so far in institution theory followed mainly algebraic-specification goals, studying properties relevant for the modularity, compositionality, and behavior of systems. However, our results contribute abstract model theory as well, notably on logic-independent Craig interpolation.

## Publications with Abstracts

**A Semantic Approach to Interpolation**- Andrei Popescu, Traian Florin Serbanuta and Grigore Rosu
, Volume 410(12-13), pp 1109-1128. 2009**J. of TCS**

*Abstract.*Craig interpolation is investigated for various types of formulae. By shifting the focus from syntactic to semantic interpolation, we generate, prove and classify a series of interpolation results for ﬁrst-order logic. A few of these results non-trivially generalize known interpolation results; all the others are new. We also discuss some applications of our results to the theory of institutions and of algebraic speciﬁcations, and a Craig-Robinson version of these results.

- PDF, J.TCS, BIB
**Behavioral Extensions of Institutions**- Andrei Popescu and Grigore Rosu
, LNCS 3629, pp. 331-347. 2005**CALCO'05**

*Abstract.*We show that any institution satisfying some reasonable conditions can be transformed into another institution, . This transformation captures formally and abstractly the intuitions of adding support for behavioral equivalence and reasoning to an existing, particular algebraic framework. We call our transformation an "extension" because has the same sentences as and because its entailment relation includes that of . Many properties of behavioral equivalence in concrete hidden logics follow as special cases of corresponding institutional results. As expected, the presented constructions and results can be instantiated to other logics satisfying our requirements as well, thus leading to novel behavioral logics, such as partial, infinitary, or second-order ones, that have the desired properties.

- PDF, CALCO'05 Slides, LNCS , CALCO '05, DBLP, BIB
**Hidden Logic**- Grigore Rosu
, University of California at San Diego**PhD Thesis**

*Abstract.*Cleverly designed software often fails to satisfy its requirements strictly, but instead satisfies them behaviorally, in the sense that they appear to be satisfied under every experiment that can be performed on the system. It is therefore becoming increasingly important to develop powerful techniques for behavioral specification and verification of systems, especially in the design stage, where most of the errors appear.

The general context of this thesis is formal methods for software and/or hardware development. We will present a promising new logic together with a language to support it, with applications to various branches of computer science, especially to the specification and automated verification of object-oriented and concurrent systems.

The thesis can be roughly divided into three major parts. The first is dedicated to presenting hidden logic in an easy going and intuitive way, with many examples, to developing sound inference rules, including a series of non-trivial*coinduction*rules, and to presenting a specification language in the OBJ family, called BOBJ, supporting hidden logic and reasoning. The second part is on automation of behavioral reasoning; more precisely, it introduces the techniques called*behavioral rewriting*,*behavioral coinductive rewriting*and*circular coinductive rewriting*, which are implemented in BOBJ. The third and the last part relates to more theoretical aspects of the logic, including relationships with other formalisms and theories, such as information hiding, coalgebra, institutions, Birkhoff-like axiomatizability, and incompleteness.

## Related External Links

- Joseph Goguen's institutions page
- The FIRTS initiative page - the 'I' in FLIRTS stands for 'Institutions'
- Razvan Diaconescu's publication list - contains recent work on institutional model theory