Structured theories and institutions

Fancisco Durán, José Meseguer

Research output: Contribution to journalConference articlepeer-review

Abstract

Category theory provides an excellent foundation for studying structured specifications and their composition. For example, theories can be structured together in a diagram, and their composition can be obtained as a colimit. There is, however, a growing awareness, both in theory and in practice, that structured theories should not be viewed just as the "scaffolding" used to build unstructured theories: they should become first-class citizens in the specification process. Given a logic formalized as an institution I, we therefore ask whether there is a good definition of the category of structured I-theories, and whether they can be naturally regarded as the ordinary theories of an appropriate institution S(I) generalizing the original institution I. We answer both questions in the affirmative, and study good properties of the institution I inherited by S(I). We show that, under natural conditions, a number of important properties are indeed inherited, including cocompleteness of the category of theories, liberality, and extension of the basic framework by free-ness constraints. The results presented here have been used as a foundation for the module algebra of the Maude language, and seem promising as a semantic basis for a generic module algebra that could be both specified and executed within the logical framework of rewriting logic. We are grateful to Narciso Martí -Oliet, Peter Mosses, and the anonymous referees for their careful reading of a previous version and for many useful suggestions to improve the exposition.

Original languageEnglish (US)
Pages (from-to)23-41
Number of pages19
JournalElectronic Notes in Theoretical Computer Science
Volume29
DOIs
StatePublished - 1999
Externally publishedYes
EventCTCS '99, Conference on Category Theory and Computer Science - Edinburgh, United Kingdom
Duration: Dec 10 1999Dec 12 1999

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Structured theories and institutions'. Together they form a unique fingerprint.

Cite this