ICFP 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Mon 13 Oct 2025 17:15 - 17:40 at Orchid West - Semantics Chair(s): Henning Urbat

Small-step and big-step operational semantics are two fundamental styles of structural operational semantics (SOS), extensively used in practice. The former one is more fine-grained and is usually regarded as primitive, as it only defines a one-step reduction relation between a given program and its direct descendant under an ambient evaluation strategy. The latter one implements, in a self-contained manner, such a strategy directly by relating a program to the net result of the evaluation process. The agreement between these two styles of semantics is one of the key pillars in operational reasoning on programs; however, such agreement is typically proven from scratch every time on a case-by-case basis. A general, abstract mathematical argument behind this agreement is up till now missing. We cope with this issue within the framework of higher-order mathematical operational semantics by providing an abstract categorical notion of big-step SOS, complementing the existing notion of abstract higher-order GSOS. Moreover, we introduce a general construction for deriving the former from the latter, and prove an abstract equivalence result between the two.

Mon 13 Oct

Displayed time zone: Perth change

16:00 - 17:40
SemanticsJFP First Papers / ICFP Papers at Orchid West
Chair(s): Henning Urbat Friedrich-Alexander University Erlangen-Nürnberg
16:00
25m
Paper
A contextual formalization of structural coinduction
JFP First Papers
Paul Downen University of Massachusetts at Lowell, Zena M. Ariola University of Oregon
DOI
16:25
25m
Paper
A practical formalization of monadic equational reasoning in dependent-type theory
JFP First Papers
Reynald Affeldt National Institute of Advanced Industrial Science and Technology (AIST), Japan, Jacques Garrigue Nagoya University, Takafumi Saikawa Nagoya University
DOI File Attached
16:50
25m
Talk
Almost Fair Simulations
ICFP Papers
Arthur Correnson CISPA Helmholtz Center for Information Security, Iona Kuhn Saarland University, Bernd Finkbeiner CISPA Helmholtz Center for Information Security
DOI
17:15
25m
Talk
Big Steps in Higher-Order Mathematical Operational Semantics
ICFP Papers
Sergey Goncharov University of Birmingham, Pouya Partow Birmingham University, Stelios Tsampas University of Southern Denmark
DOI