The aim of this FLIRTS bibliography is to
help the spreading of information through the community and encourage
the application of the theory by fellow researchers who are not FLIRTS
experts as well as the further development of the FLIRTS foundational
Complete bibliography (BiBTeX)
the bibliography (through the interface of The
Collection of Computer Science Bibliographies)
Using the keywords in
the BiBTeX entries, the bibliography is divided into the following
(partly overlapping) sections:
Categories. Just a few references about category
theory and FLIRTS-relevant results. This section (in contrast to the other ones) does not aim at being complete.
Moreover, it is not suitable as an introduction to category theory; if you need
one, see here.
Metaformalisms. Here, you can find the
seminal paper of Goguen and Burstall introducing the notion of institution,
as well as other meta-formalisms like entailment systems and logics (which
also include proof theory), specification frames (which omit the logic),
parchments (algebraic presentations of institutions) and so on.
Logics. A vast number of logics has been formalized
as institutions. Sometimes, e.g. for behavioural satisfaction, it is a
challenge to find a formulation that ensures the satisfaction condition.
Institution-independent Model Theory. It
is possible to formulate concepts such as strucured specifications, parameterization,
implementation, refinement, development etc., together with their model
theory, in a way that is completely independent of the underlying institution.
Institution-independent Proof theory. Using
the notion of entailment system (also called Pi-institution), also proof
theoretic concepts (like proof calculi for structured specifications, or
interpolation properties) and results (e.g. completeness) can be stated
in a logic-independent way.
Metatheorems about institutions, like existence
of (co)limits of institutions, characterization results about (co)freeness,
compactness, and so on.
Morphisms. Institutions can be related via
different kinds of morphisms, comorphisms, transformations, etc.
Important applications are borrowing of logical
structure, combination of logics and heterogeneous specification.
Combination (also called fibring). It is
possible to combine institutions via limits, but the resulting feature
interaction is very poor. A better feature interaction is achieved with
more specialized metaformalism categories, such as various variants of
parchments, interpretation systems, etc.
Heterogeneity. Heterogeneous specification
allows to use several logics (related via morphisms) in parallel. The possible
feature interaction is weaker than for the case of combination, but the
technical machinery is simpler and wider applicable than that for combination.
Please send new entries (which should follow a specifc format),
suggestions and comments to:
Till Mossakowski firstname.lastname@example.org
Last Updated: 06 May 2002