FLIRTS

Abstract of Talks

(In lexicographic order w.r.t. speakers)

Mapping logical systems

Maura Cerioli
In all categorical approaches, objects are characterized essentially by the acceptable maps among them; however many different notions of arrows among logical components have been defined in the last years, most (all) of them well motivated by examples and applications.

This suggests that a unifying concept of map should exist, characterizing the nature of logical components as objects, from which the other definitions of arrows are derived by specialization or some (categorical) constructions. The identification of such a ``primitive'' notion of map, in my opinion, is led by three criteria:

Thus I started to investigate from this point of view the different definitions of arrows between institutions (that are the logical components more studied so far), trying to reduce them to a "common denominator".

I'll present my (absolutely incomplete) results so far.

Mapping between categories of theories in different institutions

José Fiadeiro joint work with Mario Arrais
The necessity to deal simultaneously with different formalisms seems to be intrinsic to the discipline of Software Engineering, particularly in relation to modularity, reusability and incrementality. In order to accommodate this diversity of formalisms, we equate specification formalisms with categories of theories in different institutions and investigate functorial relationships between these categories, namely the existence of adjunctions. Linear and branching temporal logic, and deontic action logic are used as examples.

Is there a common notion of FLIRTS?

Till Mossakowski
Maura Cerioli and José Meseguer provide a family of categories of FLIRTS, at different levels, with deep results connecting them, giving a whole diagram of FLIRTS.

During my work on partial algebras, I have got some experience with some categories of FLIRTS. Based on this, in the talk I want to discuss some aspects of usefulness of the categories of FLIRTS w.r.t. to examples. Also, I want to indicate some strategies for preventing the invention of yet another notion of FLIRTS if this is not really necessary:

This is illustrated by discussing the distinction between signatures and sentences in institutions, which sometimes has been criticized as arbitrary. The talk is not intended to present final results and opinions, but to continue an ongoing discussion. A short ps paper about the talk is also available. Moreover the draft (and soon the revised) paper is available in postscript format and will be presented at the ICALP 96 conference.

Institutions with Contexts

Wieslaw Pawlowski
The talk presents a variant of the notion of institution. Institutions with contexts are ``concrete'' institutions in which it is easy to talk about things like open formulae, valuations and various types of consequence relations. This talk evolved in a paper. The draft is available on the net as gzipped postscript file

Operations for Modularly Defining Institutions

Gianna Reggio
We present some operations among institutions, used to modularly define the various formalisms developed for the SMoLCS method for the specification of concurrent systems, that since covers different phases of the development process and different kinds of systems cannot rely on a single formalism.

The institutions defined using such operations essentially share the models, which are in general subclasses of a variant of dynamic algebras (to be intended algebras of dynamic elements); while strongly differ for the formulas, ranging from positive conditional axioms, to first-order axioms in which temporal and deontic combinators appear.

Some examples, taken by case studies in the field of the specification of concurrent systems, shown the need and the convenience of having such operations.

Signature morphisms considered harmful: adjunctions between logics

Cristina Sernadas joint work with Amí lcar Sernadas
Examples show that we need morphisms (between theories, between logics, etc) that are NOT induced by signature morphisms. We propose an alternative notion of logic where signature morphisms are disregarded. A logic is considered to be a full subcategory of the logic universe at hand: either satisfaction systems, or consequence systems or theory spaces. We study both translation and bitranslation morphisms between logics. The latter are shown to induce adjunctions. The former are the basis for combining logics (limits).

Slides of this presentation are available through anonymous ftp at the Sernadas ftp page in dvi or postscript format.

Moving between logical systems

Andrzej Tarlecki
I will talk about various concepts of a morphism between institutions and their potential role in building institutions in a systematic way, in working with specifications spanning a number of institutions, in software developments migrating from one institution to another, in representing one institution in another for example to re-use proof systems available there, etc.

Are there reasons for a concept like Institutional Frames?

Uwe Wolter
The main idea of the concept ``Institutional Frame'' was to look at logical formalisms on a level of abstraction lying between the concepts ``Institution'' and ``Specification Frame''. The talk will present the reasons for introducing this concept and will address possible disadvantages and benefits.

Building institutions of dynamic data-types

Elena Zucca
We show a canonical construction which, starting from a so-called "static framework" (an institution for specifying static data structures, e.g. an algebraic institution), gives a corresponding "dynamic framework". A dynamic framework is an institution where models are sets of configurations (states in the life of the system) enriched by dynamic operations expressing dynamic evolution from one configuration into another. Any configuration can be viewed as a model in the underlying static framework ("state-as-algebra" approach). We consider three kinds of basic sentences whose satisfaction can be defined starting from the static satisfaction notion: invariant sentences (sentences in the underlying static framework considered to be satisfied iff they are satisfied by any configuration), pre-post sentences, which are a generalization of Hoare's triples, and dynamic equations, which are equalities of dynamic terms (terms involving dynamic operations), satisfied by a dynamic structure iff the two sides evaluate to the same transformation of configurations. The talk evolved in a paper; a draft is available as compressed postscript file (162142 Kb)
Please send suggestions and comments to:
Maura Cerioli cerioli@disi.unige.it

Last Updated: Monday 27 November 1995