POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
POPL 2026 (series) / le Couvent des Jacobins /

Room information: Salle 19

Venuele Couvent des Jacobins
Room nameSalle 19
Floor2
Capacity70
Room InformationNo extra information available
Program

This program is tentative and subject to change.

You're viewing the program in a time zone which is different from your device's time zone change time zone

Sun 11 Jan

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

09:00 - 10:00
KeynotePriSC at Salle 19
Chair(s): Marco Vassena Utrecht University
09:00
5m
Day opening
Day opening
PriSC

09:05
55m
Keynote
The V8 Sandbox: From Compiler Correctness to Runtime Containment
PriSC
Samuel Groß Google
10:00 - 10:30
Information Flow ControlPriSC at Salle 19
Chair(s): David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag
11:00 - 12:30
Secure Compilation & VerificationPriSC at Salle 19
Chair(s): David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag
11:00
18m
Talk
Mind the Boundary: Detecting Undefined Behavior Across Rust’s FFI
PriSC
Andreea Costea TU Delft
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
Basile Schlosser ENS Paris-Saclay, Jérémy Thibault EPFL, Cătălin Hriţcu MPI-SP
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
14:00 - 15:30
Timing Side ChannelsPriSC at Salle 19
Chair(s): Cătălin Hriţcu MPI-SP
14:00
18m
Talk
Efficient Dependency Resolution in IFC-aware Decentralized Programming
PriSC
Steffan Sølvsten Aarhus University, Aslan Askarov Aarhus University
14:18
18m
Talk
Tooling Design and Lessons Learned from Systematic Evaluations of the Preservation of Low-level Security Properties by Compilers with BinSec
PriSC
Yanis Sellami CEA, List, Univ. Grenoble Alpes, Frédéric Recoules CEA, List, Sébastien Bardin CEA LIST, University Paris-Saclay
14:36
18m
Talk
Decompiling for Constant-Time Analysis
PriSC
Sören van der Wall TU Braunschweig, Santiago Arranz Olmos Max Planck Institute for Security and Privacy, Gilles Barthe MPI-SP; IMDEA Software Institute, Lionel Blatter Max Planck Institute for Security and Privacy, Youcef Bouzid , Zhiyuan Zhang
14:54
18m
Talk
Modular Verification of Probabilistic Constant-Time
PriSC
Xingyu Xie MPI-SP
15:12
18m
Talk
GnuZero: A Compiler-Based Zeroization Static Detection Tool for the Masses
PriSC
Pierrick Philippe Univ Rennes, CNRS, IRISA, Mohamed Sabt Univ Rennes, CNRS, IRISA, Pierre-Alain Fouque Univ Rennes, CNRS, IRISA
16:00 - 17:30
Hardware SecurityPriSC at Salle 19
Chair(s): Jérémy Thibault EPFL
16:00
18m
Talk
FSLH: Flexible Mechanized Speculative Load Hardening
PriSC
Jonathan Baumann MPI-SP, Roberto Blanco Max Planck Institute for Security and Privacy (MPI-SP), Léon Ducruet Aarhus University, Sebastian Harwig MPI-SP and Ruhr University Bochum, Cătălin Hriţcu MPI-SP
16:18
18m
Talk
Towards Robust Secure Compilation in Presence of Speculative Execution
PriSC
Léopold Clément Télécom Paris, Ulrich Kühne Télécom Paris, Florian Brandner Télécom Paris, Renaud Pacalet Télécom Paris
16:36
18m
Talk
Compiling countermeasures against fault attacks with “Tracing LLVM”
PriSC
Sébastien Michelland Université Grenoble-Alpes - Grenoble INP - LCIS, Christophe Deleuze Université Grenoble-Alpes - Grenoble INP - LCIS, Laure Gonnord Université Grenoble-Alpes - Grenoble INP - LCIS
File Attached
16:54
18m
Talk
Modular and automatic formal verification of a RISC-V processor with security mechanisms
PriSC
Pierre Wilke CentraleSupélec, Cyprien Jules CentraleSupélec, Inria, CNRS, Univ. Rennes, Guillaume Hiet CentraleSupélec, Inria, CNRS, Univ. Rennes
17:12
18m
Talk
Fun with flags: How Compilers Break and Fix Constant-Time Code
PriSC
Antoine Geimer Univ. Lille, CNRS, Inria, Clémentine Maurice Univ. Lille, Inria, CNRS
17:30 - 18:00
Lightning TalksPriSC at Salle 19
Chair(s): Lesly-Ann Daniel EURECOM
17:30
25m
Talk
Lightning Talks
PriSC

17:55
5m
Day closing
Day closing
PriSC

Mon 12 Jan

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

14:00 - 15:30
A Guided Tour through Oxidized OCamlTutorials at Salle 19
14:00
90m
Tutorial
A Guided Tour through Oxidized OCaml
Tutorials
Gavin Gray Brown University, Anil Madhavapeddy University of Cambridge, UK, KC Sivaramakrishnan IIT Madras and Tarides, Will Crichton Brown University, Shriram Krishnamurthi Brown University, Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street
16:00 - 17:30
A Guided Tour through Oxidized OCamlTutorials at Salle 19
16:00
90m
Tutorial
A Guided Tour through Oxidized OCaml
Tutorials
Gavin Gray Brown University, Anil Madhavapeddy University of Cambridge, UK, KC Sivaramakrishnan IIT Madras and Tarides, Will Crichton Brown University, Shriram Krishnamurthi Brown University, Chris Casinghino Jane Street, Richard A. Eisenberg Jane Street

Tue 13 Jan

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

09:00 - 10:30
Types and logicsPEPM at Salle 19
Chair(s): Yukiyoshi Kameyama University of Tsukuba
09:00
5m
Day opening
Welcome
PEPM
Yukiyoshi Kameyama University of Tsukuba, Ningning Xie University of Toronto
09:05
30m
Research paper
Hole Refinements for Polymorphic Type-and-Example Driven Synthesis
PEPM
Niek Mulleners Utrecht University, Johan Jeuring Utrecht University, Wouter Swierstra Utrecht University, Netherlands
DOI
09:35
30m
Research paper
Inferring Typing Rules for Contextual Sugars
PEPM
Tailai Yu Peking University, Zhichao Guan Peking University, Di Wang Peking University, Zhenjiang Hu Peking University
DOI
10:05
15m
Short-paper
S4 modal sequent calculus as intermediate logic and intermediate language (Short Paper)
PEPM
Jean Caspar École normale supérieure – PSL, INRIA, LS2N, CNRS, Guillaume Munch-Maccagnoni INRIA
File Attached
10:20
15m
Short-paper
Epistemic Logic for Polyglots (Short Paper)
PEPM
Luis Garcia , Chris Martens Northeastern University
File Attached
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
14:00 - 15:30
KeynotePEPM at Salle 19
Chair(s): Ningning Xie University of Toronto
14:00
90m
Keynote
Revisiting the Evolution of Effects (Invited Talk)Keynote
PEPM
Nicolas Wu Imperial College London
DOI
16:00 - 17:30
Staging and effect handlersPEPM at Salle 19
Chair(s): Sam Lindley University of Edinburgh
16:00
30m
Research paper
Staging Effect Handlers for Modular Search
PEPM
Alexandru Trifanov Independent, Tom Schrijvers KU Leuven
DOI
16:30
15m
Talk
Holey: Staged Execution from Python to SMT (Talk Proposal)
PEPM
Nada Amin Harvard University
16:45
15m
Short-paper
Towards Cumulative Abstract Semantics via Handlers (Short Paper)
PEPM
Cade Lueker University of Colorado Boulder, Andrew Fox University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon
File Attached
17:00
15m
Short-paper
Retargeting an Abstract Interpreter for a New Language by Partial Evaluation (Short Paper)
PEPM
Jay Lee Seoul National University, Joongwon Ahn Seoul National University, Kwangkeun Yi Seoul National University
File Attached
17:15
10m
Day closing
Closing
PEPM
Yukiyoshi Kameyama University of Tsukuba, Ningning Xie University of Toronto

Sat 17 Jan

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

09:00 - 10:30
Opening and KeynoteGiacoFest at Salle 19
Chair(s): Mila Dalla Preda University of Verona
09:10
10m
Talk
Opening
GiacoFest

09:20
70m
Talk
Keynote Speech
GiacoFest

11:00 - 12:30
Short TalksGiacoFest at Salle 19
Chair(s): Marco Campion Inria Paris - ENS - Université PSL, Michele Pasqua University of Verona
11:00
90m
Talk
Short Talks
GiacoFest

Hide past events

Sun 11 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Salle 19

PriSC

Keynote

PriSC

Information Flow Control

PriSC

Secure Compilation & Verification

PriSC

Timing Side Channels

PriSC

Hardware Security

PriSC

Lightning Talks

Mon 12 Jan

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

Room14:003015:003016:003017:0030
Salle 19

Tutorials

A Guided Tour through Oxidized OCaml

Tutorials

A Guided Tour through Oxidized OCaml

Tue 13 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Salle 19

PEPM

Types and logics

PEPM

Semantics and applications

PEPM

Keynote

PEPM

Staging and effect handlers

Sat 17 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Salle 19

GiacoFest

Opening and Keynote

GiacoFest

Short Talks

GiacoFest

GiacoFest

Hide past events

Sun 11 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Salle 19
PriSC
Day opening
09:00 - 09:05
PriSC
The V8 Sandbox: From Compiler Correctness to Runtime Containment
09:05 - 10:00
PriSC
Mind the Boundary: Detecting Undefined Behavior Across Rust’s FFI
11:00 - 11:18
PriSC
Specifying ABIs with Realizability and Type-Preserving Compilation
11:18 - 11:36
PriSC
Towards formally secure compilation of verified F* programs against unv ...
11:36 - 11:54
PriSC
Blame-aware Recomposition for Formally Secure Low-level Compiler Backends
11:54 - 12:12
PriSC
WP-Preserving Compilation -- Preserving Weakest Preconditions For End-t ...
12:12 - 12:30
PriSC
Efficient Dependency Resolution in IFC-aware Decentralized Programming
14:00 - 14:18
PriSC
Tooling Design and Lessons Learned from Systematic Evaluations of the P ...
14:18 - 14:36
PriSC
Decompiling for Constant-Time Analysis
14:36 - 14:54
PriSC
Modular Verification of Probabilistic Constant-Time
14:54 - 15:12
PriSC
GnuZero: A Compiler-Based Zeroization Static Detection Tool for the Masses
15:12 - 15:30
PriSC
FSLH: Flexible Mechanized Speculative Load Hardening
16:00 - 16:18
PriSC
Towards Robust Secure Compilation in Presence of Speculative Execution
16:18 - 16:36
PriSC
Compiling countermeasures against fault attacks with “Tracing LLVM”
16:36 - 16:54
PriSC
Modular and automatic formal verification of a RISC-V processor with se ...
16:54 - 17:12
PriSC
Fun with flags: How Compilers Break and Fix Constant-Time Code
17:12 - 17:30
PriSC
Lightning Talks
17:30 - 17:55
PriSC
Day closing
17:55 - 18:00

Mon 12 Jan

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

Room14:0015304515:0015304516:0015304517:00153045
Salle 19
POPL Tutorials
A Guided Tour through Oxidized OCaml
14:00 - 15:30
POPL Tutorials
A Guided Tour through Oxidized OCaml
16:00 - 17:30

Tue 13 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Salle 19
PEPM
Welcome
09:00 - 09:05
PEPM
Hole Refinements for Polymorphic Type-and-Example Driven Synthesis
09:05 - 09:35
PEPM
Inferring Typing Rules for Contextual Sugars
09:35 - 10:05
PEPM
S4 modal sequent calculus as intermediate logic and intermediate langua ...
10:05 - 10:20
PEPM
Epistemic Logic for Polyglots (Short Paper)
10:20 - 10:35
PEPM
Computation-Tree Semantics: An Algorithmic Approach to Structurally Def ...
11:00 - 11:30
PEPM
Towards Lightweight and Efficient Choreographic Cloud Services
11:30 - 12:00
PEPM
Incrementalizing Haskell implementation of Putback-based Bidirectional ...
12:00 - 12:15
PEPM
Partial Evaluation as a primitive in modern network troubleshooting (Ta ...
12:15 - 12:30
PEPMKeynote
Revisiting the Evolution of Effects (Invited Talk)
14:00 - 15:30
PEPM
Staging Effect Handlers for Modular Search
16:00 - 16:30
PEPM
Holey: Staged Execution from Python to SMT (Talk Proposal)
16:30 - 16:45
PEPM
Towards Cumulative Abstract Semantics via Handlers (Short Paper)
16:45 - 17:00
PEPM
Retargeting an Abstract Interpreter for a New Language by Partial Evalu ...
17:00 - 17:15
PEPM
Closing
17:15 - 17:25

Sat 17 Jan

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

Room9:0015304510:0015304511:0015304512:00153045
Salle 19
GiacoFest
Opening
09:10 - 09:20
GiacoFest
Keynote Speech
09:20 - 10:30
GiacoFest
Short Talks
11:00 - 12:30
Hide past events