License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2022.30
URN: urn:nbn:de:0030-drops-163111
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16311/
Go to the corresponding LIPIcs Volume Portal

Goncharov, Sergey ; Milius, Stefan ; Schröder, Lutz ; Tsampas, Stelios ; Urbat, Henning

Stateful Structural Operational Semantics

pdf-format:
LIPIcs-FSCD-2022-30.pdf (0.8 MB)

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 compositionality of the two more abstract equivalences.

BibTeX - Entry

@InProceedings{goncharov_et_al:LIPIcs.FSCD.2022.30,
  author =	{Goncharov, Sergey and Milius, Stefan and Schr\"{o}der, Lutz and Tsampas, Stelios and Urbat, Henning},
  title =	{{Stateful Structural Operational Semantics}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{30:1--30:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16311},
  URN =		{urn:nbn:de:0030-drops-163111},
  doi =		{10.4230/LIPIcs.FSCD.2022.30},
  annote =	{Keywords: Structural Operational Semantics, Rule Formats, Distributive Laws}
}

Keywords: Structural Operational Semantics, Rule Formats, Distributive Laws
Collection: 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Issue Date: 2022
Date of publication: 28.06.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI