Abstract semantics for K module composition

Codruta Girlea, Grigore Rosu

Research output: Contribution to journalArticlepeer-review


A structured K definition is easier to write, understand and debug than one single module containing the whole definition. Furthermore, modularization makes it easy to reuse work between definitions that share some principles or features. Therefore, it is useful to have a semantics for module composition operations that allows the properties of the resulting modules to be well understood at every step of the composition process. This paper presents an abstract semantics for a module system proposal for the K framework. It describes K modules and module transformations in terms of institution-based model theory introduced by Goguen and Burstall.

Original languageEnglish (US)
Pages (from-to)127-149
Number of pages23
JournalElectronic Notes in Theoretical Computer Science
StatePublished - Jun 10 2014


  • Abstract Modules
  • Institutions
  • K
  • Module System
  • Semantics

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Abstract semantics for K module composition'. Together they form a unique fingerprint.

Cite this