FLIRTS
Abstract of Talks
(In lexicographic order w.r.t. speakers)
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:

the correspondence between limit/colimit constructions and their intuitive
counterpart; for example a "subobject" can be expected to be a sort of
setcontained component.

the capability to derive from this particular concept (most of) the other notions
of maps.

the capability to capture the known examples of interesting maps between actual
components.
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.
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.
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:

rather than invent a new notion of FLIRTS, use a subcategory of
some known category of FLIRTS

or use some monadic construction on such a category

and try to add your notions to the above diagram
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.
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
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 firstorder 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.
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.
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 reuse proof
systems available there, etc.
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.
Elena Zucca
We show a canonical construction which, starting from a socalled
"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 ("stateasalgebra" 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), prepost 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