Maude’s module algebra

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.