FLIRTS Bibliography

Complete bibliography (BiBTeX)   BiBTeX.gz

Search 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.