ICFP 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025

This program is tentative and subject to change.

Mon 13 Oct 2025 17:15 - 17:40 at Orchid West - Semantics

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.

This program is tentative and subject to change.

Mon 13 Oct

Displayed time zone: Perth change

16:00 - 17:40
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 , Takafumi Saikawa Nagoya University
DOI
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