Maude's module algebra

Francisco Durán, José Meseguer

Research output: Contribution to journalArticlepeer-review


The reflective capabilities of rewriting logic and their efficient implementation in the Maude language can be exploited to endow a reflective language like Maude with a module algebra in which structured theories can be combined and transformed by means of a rich collection of module operations. We have followed this approach and have used the specification of such a module algebra as its implementation, including a user interface and an execution environment for it. The high level at which the specification of the module algebra has been given makes this approach particularly attractive when compared to conventional implementations, because of its shorter development time and the greater flexibility, maintainability, and extensibility that it affords. We explain the general principles of the reflective design of the module algebra and its categorical foundations, based on the institution-theoretic notion of structured theory and morphisms and colimits for such theories. Based on such foundations, we then explain the categorical semantics of Maude's parameterized theories, modules and views and their instantiation, and the reflective algebraic specification of the different module and view operations.

Original languageEnglish (US)
Pages (from-to)125-153
Number of pages29
JournalScience of Computer Programming
Issue number2
StatePublished - Apr 30 2007


  • Institutions
  • Maude
  • Membership equational logic
  • Module algebra
  • Parameterization
  • Reflection
  • Rewriting logic
  • Structured theories

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Maude's module algebra'. Together they form a unique fingerprint.

Cite this