Summary of: Dynamic Structural Operational Semantics

Abstract

This short paper summarises the contributions published in the authors’ journal article [2]. The journal paper develops the theory of Dynamic Structural Operational Semantics (DSOS or Dynamic SOS) as a framework for describing semantics of programming languages that include dynamic software upgrades. DSOS is built on top of the Modular SOS since it allows a sharp separation of the program execution code from the additional structures needed at run-time. DSOS follows the same modularity and decoupling that MSOS advocates, partly motivated by the long term goal of having machine-checkable proofs for general results like type safety. Dynamic SOS has been applied on two languages supporting dynamic software upgrades, namely the low-level Proteus, which supports updating of variables, functions, records, or types at specific program points, and Creol, which supports dynamic class upgrades in the setting of concurrent objects. Existing type analyses for software upgrades can be done on top of DSOS too, as we illustrate for Proteus.