Stateful Structural Operational Semantics
Sergey Goncharov, Stefan Milius, Lutz Schr\"oder, Stelios Tsampas and, Henning Urbat

TL;DR
This paper introduces a new stateful SOS rule format that guarantees compositionality for certain abstract semantics in programming languages, addressing limitations of existing approaches.
Contribution
It proposes the cool stateful SOS formats that ensure compositionality of more coarse-grained semantics in stateful programming languages.
Findings
Streamlined stateful SOS formats guarantee compositionality.
Undecidability persists for certain semantics despite restrictions.
New rule formats extend the applicability of compositional semantics.
Abstract
Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very fine-grained equivalences that essentially assume unrestricted interference by the environment between any two statements. We introduce the more restrictive stateful SOS rule format for stateful languages. We show that compositionality of two more coarse-grained semantics, respectively given by assuming read-only interference or no interference between steps, remains an undecidable property even for stateful SOS. However, further restricting the rule format in a manner inspired by the cool GSOS formats of Bloom and van Glabbeek, we obtain the streamlined and cool stateful SOS formats, which respectively guarantee…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
