Computation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
Structural operational semantics (SOS) is one of the most common formalisms for specifying language semantics. There has been much interest in automatically deriving small-step SOS definitions from big-step definitions and vice versa, as well as towards extrapolating language implementations from these inductive, declarative definitions. This work presents Computation-Tree Semantics (CTS) in which semantic configurations are tree-structured, unlike standard SOS-configurations which are “flat”. This tree-structure is key in making our approach algorithmic, meaning it is able to describe how a transition is produced, contrary to the traditional declarative approach taken by SOS. We show how one can – in a straight-forward manner – obtain a CTS from the big-step semantics of a simple arithmetic language, a simple while language, and the call-by-need lambda-calculus as given by Launchbury. From the resulting CTS, we then obtain a small-step understanding of all these languages. The arithmetic language example is formalised in Coq/Rocq.
Tue 13 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
11:00 - 12:30 | |||
11:00 30mResearch paper | Computation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations PEPM DOI | ||
11:30 30mResearch paper | Towards Lightweight and Efficient Choreographic Cloud Services PEPM Alex Ionescu Chalmers University of Technology; University of Gothenburg, Alejandro Russo Chalmers University of Technology; University of Gothenburg DOI | ||
12:00 15mShort-paper | Incrementalizing Haskell implementation of Putback-based Bidirectional Transformation Language BiGUL (Short Paper) PEPM File Attached | ||
12:15 15mTalk | Partial Evaluation as a primitive in modern network troubleshooting (Talk Proposal) PEPM Anduo Wang Temple University, USA | ||