POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Tue 13 Jan 2026 11:00 - 11:30 at Salle 19 - Semantics and applications Chair(s): Meng Wang

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 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

11:00 - 12:30
Semantics and applicationsPEPM at Salle 19
Chair(s): Meng Wang University of Bristol
11:00
30m
Research paper
Computation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
PEPM
Sean Kristian Remond Harbo Aalborg University, Hans Hüttel Aalborg University
DOI
11:30
30m
Research 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
15m
Short-paper
Incrementalizing Haskell implementation of Putback-based Bidirectional Transformation Language BiGUL (Short Paper)
PEPM
Masaki Toyoda Hosei University, Soichiro Hidaka Hosei University
File Attached
12:15
15m
Talk
Partial Evaluation as a primitive in modern network troubleshooting (Talk Proposal)
PEPM
Anduo Wang Temple University, USA