POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Thu 15 Jan 2026 16:10 - 16:35 at Nef - Verified Compilation Chair(s): Clément Pit-Claudel

Simulations are widely-used notions of program refinement. This paper discusses and compares several of them, in particular notions of simulation that are both weak and sensitive to divergence. Complex simulation proofs performed in proof assistants, for instance in a verified compilation setting, often rely on variants of normed simulation, which is not complete with respect to divergence-sensitive weak simulation. We propose to bridge this gap with µdiv-simulation, a novel notion of simulation that is equivalent to classical divergence-sensitive weak simulation, and designed to be as comfortable to use as modern characterizations of normed simulation. We then define a parameterized notion of simulation that covers strong simulation, weak simulation, µdiv-simulation, and 9 more notions of simulation, and jointly establish various "up-to" reasoning techniques for these 12 notions. Our results are formalized in Rocq and instantiated on two case studies: Choice Trees and a CompCert pass. Verified compilation is a major motivation for our study, but because we work with an abstract LTS setting, our results are also relevant to other fields that make use of divergence-sensitive weak simulation, such as model checking.

Thu 15 Jan

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

16:10 - 17:00
Verified CompilationPOPL at Nef
Chair(s): Clément Pit-Claudel EPFL
16:10
25m
Talk
A Family of Sims with Diverging Interests
POPL
Nicolas Chappe CNRS - Verimag
DOI
16:35
25m
Talk
Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation
POPL
Niklas Mück MPI-SWS, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS, Michael Sammler Institute of Science and Technology Austria
DOI Pre-print