WG211/M20Mosses
Modular SOS and static semantics
At the meeting in Kyoto, I talked about the CBS framework (slides), which supports specification of programming languages by translation to an open-ended collection of so-called 'funcons' (language-independent fundamental programming constructs). The dynamic semantics of funcons has been defined in a modular variant of structural operational semantics. As mentioned in the conclusion of that talk, it was unclear how to give modular definitions of the static semantics of funcons, allowing arbitrary effects as well as types.
After recalling the main features of Modular SOS, I will present MTES, a modular variant of conventional type and effect systems. In MTES, static semantic entities approximate how corresponding dynamic entities flow in Modular SOS. When the collection of funcons is extended with new funcons that require additional semantic entities, the MSOS and MTES definitions of the original funcons do not change.
MTES has been developed in collaboration with Casper Bach Poulsen, Sebastian Erdweg, Sven Keidel, and Neil Sculthorpe.
