A Syntactic Approach to Modularity in Denotational Semantics

This paper proposes a syntactic reformulation of the modular approach to Denotational Semantics in [Mog89a, Mog91a]. This reformulation is based on a duality between model constructions and translations of theories (often called relative interpretations), analogous to Gabriel-Ulmer duality. To demonstrate the simplicity and usability of the syntactic reformulation, we give a sample of theories and translations, which can be used to give semantics to concurrent languages (via translation into suitable metalanguages). Introduction The main objective of Denotational Semantics is to provide mathematical models of programming languages. These models can be used both as formal descriptions of programming languages and also to validate reasoning principles. However, to make Denotational Semantics usable one must address two key issues: ffl Modularity. A key issue in the applicability of formalisms to large-scale examples is the ability to structure theories so as to be able to reuse compone..