Institutions

From FSL
Jump to: navigation, search

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
J. of TCS, Volume 410(12-13), pp 1109-1128. 2009
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 first-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 specifications, and a Craig-Robinson version of these results.
PDF, J.TCS, BIB
Behavioral Extensions of Institutions
Andrei Popescu and Grigore Rosu
CALCO'05, LNCS 3629, pp. 331-347. 2005
Abstract. We show that any institution \mathcal{I} satisfying some reasonable conditions can be transformed into another institution, {\mathcal{I}}_{beh}. 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 {\mathcal I}_{beh} has the same sentences as \mathcal I and because its entailment relation includes that of \mathcal I. 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
PhD Thesis, University of California at San Diego
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.
PDF, Thesis@UCSD, BIB


Related External Links

Personal tools
Namespaces

Variants
Actions
Navigation