Structured theories and institutions

Francisco Durán, José Meseguer

Research output: Contribution to journalArticlepeer-review


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 script I sign, we therefore ask whether there is a good definition of the category of structured script I sign-theories, and whether they can be naturally regarded as the ordinary theories of an appropriate institution script S sign (script I sign) generalizing the original institution script I sign. We answer both questions in the affirmative, and study good properties of the institution script I sign inherited by script S sign (script I sign). 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 freeness 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.

Original languageEnglish (US)
Pages (from-to)357-380
Number of pages24
JournalTheoretical Computer Science
Issue number1-3
StatePublished - Dec 2 2003


  • Institutions
  • Maude
  • Structured theories

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


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

Cite this