POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France

This program is tentative and subject to change.

Sun 11 Jan 2026 11:18 - 11:36 at Salle 19 - Secure Compilation & Verification

Language designers and compiler developers in need of an ABI find themselves caught between two extremes: an ABI can be specified informally with prose and validated by inspection and testing, or it can be specified rigorously with a realizability model and validated by proofs. We propose a middle ground where we define a realizability model for RichWasm, indexed by RichWasm types and inhabited by WebAssembly computations—doing all the work that requires expertise in semantic models and program logics—and source-language compilers can benefit from the memory-safe ABI specified by the model by simply building a type-preserving compiler to RichWasm. Now, if there is a type-preserving compiler from a source language to RichWasm, the ABI for any source type $\tau$ is the interpretation $\llbracket\tau^+\rrbracket$ in our realizability model, where $\tau^+$ is the type translation for $\tau$. In other words, by writing a type-preserving compiler to RichWasm, a WebAssembly ABI falls out “for free!”

This program is tentative and subject to change.

Sun 11 Jan

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

11:00 - 12:30
Secure Compilation & VerificationPriSC at Salle 19
11:00
18m
Talk
Mind the Boundary: Detecting Undefined Behavior Across Rust’s FFI
PriSC
11:18
18m
Talk
Specifying ABIs with Realizability and Type-Preserving Compilation
PriSC
Brianna Marshall Northeastern University, Ryan Doenges Boston College, Owen Duckham Northeastern University, Ari Prakash Northeastern University, Maxime Legoupil Aarhus University, Elan Semenova Northeastern University, Lars Birkedal Aarhus University, Amal Ahmed Northeastern University, USA
11:36
18m
Talk
Towards formally secure compilation of verified F* programs against unverified ML contexts
PriSC
Cezar-Constantin Andrici MPI-SP, Danel Ahman University of Ljubljana, Cătălin Hriţcu MPI-SP, Guido Martínez Microsoft Research, Abigail Pribisova MPI-SP and MPI-SWS, Exequiel Rivas Tallinn University of Technology; Ahrefs, Théo Winterhalter INRIA
11:54
18m
Talk
Blame-aware Recomposition for Formally Secure Low-level Compiler Backends
PriSC
12:12
18m
Talk
WP-Preserving Compilation -- Preserving Weakest Preconditions For End-to-End Verification
PriSC
Carmine Abate Barkhausen Institute, Dresden, Mohamed Elsheikh Barkhausen Institute, Dresden, Kleio Liotati Barkhausen Institute, Dresden, Frantisek Farka Barkhausen Institute, Dresden, Sebastian Ertel Barkhausen Institute, Dresden