Towards a Module System for K

To create reusable definitions of language features, isolated from changes to other features in the language, it is important that feature definitions be modular. This abstract introduces ongoing work on modularity features in K, an algebraic, rewriting logic based formalism for defining the semantics of programming languages.

Conference paper

Proceedings of the 19th International Workshop Recent Trends in Algebraic Development Techniques (WADT 2008)