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

Room information: Belvédère

Venuele Couvent des Jacobins
Room nameBelvédère
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

Mon 12 Jan

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

09:00 - 10:30
Keynote 1 and Paper 1CPP at Belvédère
Chair(s): Nicolas Tabareau Inria
09:00
60m
Keynote
TBA
CPP
K: Amaury Hayat Ecole nationale des Ponts et Chaussées
10:08
22m
Talk
Higher order differential calculus in Mathlib
CPP
Sebastien Gouezel CNRS and Rennes University
11:00 - 12:50
Formalized mathematicsCPP at Belvédère
Chair(s): Marie Kerjean CNRS, Université Sorbonne Paris Nord, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio Inria, Université Jean Monnet Saint-Étienne
11:00
22m
Talk
Bar Inductive Predicates for Constructive Algebra in Rocq
CPP
Dominique Larchey-Wendling Université de Lorraine, CNRS, LORIA
DOI Pre-print
11:22
22m
Talk
Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq
CPP
Holger Thies Kyoto University
11:44
22m
Talk
Cylindrical Algebraic Decomposition in Coq/Rocq
CPP
Quentin Vermande Université Côte d'Azur, Inria
12:06
22m
Talk
Adhesive Category Theory for Graph Rewriting in Rocq
CPP
Samuel Arsac ENS Lyon, Russ Harmer CNRS, Damien Pous CNRS
12:28
22m
Talk
Formalizing polynomial laws and the universal divided power algebra
CPP
Antoine Chambert-Loir Université Paris Cité, María Inés de Frutos Fernández University of Bonn
14:00 - 15:30
Proof assistantsCPP at Belvédère
14:00
22m
Talk
A Certifying Proof Assistant for Synthetic Mathematics in Lean
CPP
Wojciech Nawrocki Carnegie Mellon University, Joseph Hua Carnegie Mellon University, Mario Carneiro Chalmers University of Technology, Yiming Xu LMU Munich, Spencer Woolfson Carnegie Mellon University, Shuge Rong Carnegie Mellon University, Sina Hazratpour Johns Hopkins University, Steve Awodey Carnegie Mellon University
14:22
22m
Talk
Adding Sorts to an Isabelle Formalization of Superposition
CPP
Balazs Toth Ludwig-Maximilians-Universität München, Martin Desharnais Ludwig-Maximilians-Universität München, Jasmin Blanchette Ludwig-Maximilians-Universität München
14:45
22m
Talk
A Lambda-Superposition Tactic for Isabelle/HOL
CPP
Massin Guerdi Ludwig-Maximilians-Universität München
15:07
22m
Talk
Certifying the decidability of the word problem in monoids at large
CPP
Reinis Cirpons St Andrews University, Florent Hivert Univ. Paris-Saclay, LISN, LMF, CNRS, INRIA, Assia Mahboubi INRIA, Guillaume Melquiond Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, James Mitchell St Andrews University, Finn Smith St Andrews University
16:00 - 17:30
CompilersCPP at Belvédère
16:00
22m
Talk
Mechanized Dominator Tree Certification
CPP
Jean-Christophe Léchenet Université Côte d’Azur, Inria
16:22
22m
Talk
Brack: A Verified Compiler for Scheme via CakeML
CPP
Pascal Lasnier University of Cambridge, Jeremy Yallop University of Cambridge, Magnus O. Myreen Chalmers University of Technology
16:45
22m
Talk
Verified VCG and Verified Compiler for Dafny
CPP
Daniel Nezamabadi ETH Zurich, Magnus O. Myreen Chalmers University of Technology, Yong Kiam Tan Institute for Infocomm Research, A*STAR
17:07
22m
Talk
Foundational Verification of Running-Time Bounds for Interactive Programs
CPP
Thomas Carotti MIT, Andy Tockman Massachussetts Institute of Technology, Pratap Singh CMU, Andres Erbsen Google, Samuel Gruetter ETH Zurich, Adam Chlipala Massachusetts Institute of Technology

Tue 13 Jan

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

09:00 - 10:30
Keynote 2 and Paper 2CPP at Belvédère
Chair(s): Nikhil Swamy Microsoft Research
09:00
60m
Keynote
TBA
CPP
Jennifer Paykin University of Vermont
10:00
30m
Meeting
Business Meeting
CPP
Nikhil Swamy Microsoft Research, Nicolas Tabareau Inria
11:00 - 12:50
MetatheoryCPP at Belvédère
11:00
22m
Talk
Can we formalise type theory intrinsically without any compromise? A case study in Cubical Agda
CPP
Liang-Ting Chen Academia Sinica, Fredrik Nordvall Forsberg University of Strathclyde, Tzu-Chun Tsai Academia Sinica
11:22
22m
Talk
Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions
CPP
Tomaz Mascarenhas Universidade Federal de Minas Gerais, Harun Khan Stanford University, Abdalrhman Mohamed Stanford University, Andrew Reynolds University of Iowa, Haniel Barbosa Universidade Federal de Minas Gerais, Clark Barrett Stanford University, Cesare Tinelli University of Iowa
11:44
22m
Talk
Mechanizing Synthetic Tait Computability in Istari
CPP
Runming Li Carnegie Mellon University, Yue Yao Carnegie Mellon University, Robert Harper Carnegie Mellon University
12:06
22m
Talk
Building Blocks for Step-Indexed Program Logics
CPP
Thomas Somers Radboud University Nijmegen, Jonas Kastberg Hinrichsen Aalborg University, Lennard Gäher MPI-SWS, Robbert Krebbers Radboud University Nijmegen
12:28
22m
Talk
A Rose Tree is Blooming (Proof Pearl)
CPP
Joomy Korkut Bloomberg
14:00 - 15:30
Program verificationCPP at Belvédère
14:00
22m
Talk
Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis
CPP
Shuanglong Kan Barkhausen Institute, Dresden, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS
14:22
22m
Talk
Enhancing Symbolic Execution with Machine-Checked Safety Proofs
CPP
David Trabish Technion, Shachar Itzhaky Technion
14:45
22m
Talk
Layers of Confluence for Actors
CPP
Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Einar Broch Johnsen University of Oslo, Åsmund Aqissiaq Arild Kløvstad University of Oslo (UiO), Violet Ka I Pun Western Norway University of Applied Sciences, Yannick Zakowski Inria
15:07
22m
Talk
Towards composable proofs of cache coherence protocols
CPP
Martina Camaioni EPFL, Yann Herklotz EPFL, Tz-Ching Yu EPFL, Thomas Bourgeat EPFL
16:00 - 17:30
Separation logicCPP at Belvédère
16:00
22m
Talk
A Recipe for Modular Verification of Generic Tree Traversals
CPP
Laila Elbeheiry MPI-SWS, Michael Sammler Institute of Science and Technology Austria, Robbert Krebbers Radboud University Nijmegen, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS
16:22
22m
Talk
Precise Reasoning about Container-Internal Pointers with Logical Pinning
CPP
Yawen Guan EPFL, Clément Pit-Claudel EPFL
16:45
22m
Talk
Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic
CPP
Virgil Marionneau ENS Rennes, Félix Sassus-Bourda ENS Paris Saclay, Alejandro Aguirre Aarhus University, Lars Birkedal Aarhus University
17:07
22m
Talk
Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust
CPP
Arnaud Golfouse Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire des méthodes formelles, 91190, Gif-sur-Yvette, France, Armaël Guéneau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, Jacques-Henri Jourdan CNR, LMF

Mon 12 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Belvédère

CPP

Keynote 1 and Paper 1

CPP

Formalized mathematics

CPP

Proof assistants

CPP

Compilers

Tue 13 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Belvédère

CPP

Keynote 2 and Paper 2

CPP

Metatheory

CPP

Program verification

CPP

Separation logic

Mon 12 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Belvédère
CPP
TBA
09:00 - 10:00
CPP
Higher order differential calculus in Mathlib
10:08 - 10:30
CPP
Bar Inductive Predicates for Constructive Algebra in Rocq
11:00 - 11:22
CPP
Computing Solutions for Systems of Multivariate Ordinary Differential E ...
11:22 - 11:44
CPP
Cylindrical Algebraic Decomposition in Coq/Rocq
11:44 - 12:06
CPP
Adhesive Category Theory for Graph Rewriting in Rocq
12:06 - 12:28
CPP
Formalizing polynomial laws and the universal divided power algebra
12:28 - 12:50
CPP
A Certifying Proof Assistant for Synthetic Mathematics in Lean
14:00 - 14:22
CPP
Adding Sorts to an Isabelle Formalization of Superposition
14:22 - 14:45
CPP
A Lambda-Superposition Tactic for Isabelle/HOL
14:45 - 15:07
CPP
Certifying the decidability of the word problem in monoids at large
15:07 - 15:30
CPP
Mechanized Dominator Tree Certification
16:00 - 16:22
CPP
Brack: A Verified Compiler for Scheme via CakeML
16:22 - 16:45
CPP
Verified VCG and Verified Compiler for Dafny
16:45 - 17:07
CPP
Foundational Verification of Running-Time Bounds for Interactive Programs
17:07 - 17:30

Tue 13 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Belvédère
CPP
TBA
09:00 - 10:00
CPP
Business Meeting
10:00 - 10:30
CPP
Can we formalise type theory intrinsically without any compromise? A ca ...
11:00 - 11:22
CPP
Formalization of a Proof Calculus for Incremental Linearization for Sat ...
11:22 - 11:44
CPP
Mechanizing Synthetic Tait Computability in Istari
11:44 - 12:06
CPP
Building Blocks for Step-Indexed Program Logics
12:06 - 12:28
CPP
A Rose Tree is Blooming (Proof Pearl)
12:28 - 12:50
CPP
Certified Symbolic Finite Transducers: Formalization and Applications t ...
14:00 - 14:22
CPP
Enhancing Symbolic Execution with Machine-Checked Safety Proofs
14:22 - 14:45
CPP
Layers of Confluence for Actors
14:45 - 15:07
CPP
Towards composable proofs of cache coherence protocols
15:07 - 15:30
CPP
A Recipe for Modular Verification of Generic Tree Traversals
16:00 - 16:22
CPP
Precise Reasoning about Container-Internal Pointers with Logical Pinning
16:22 - 16:45
CPP
Modular Specifications and Implementations of Random Samplers in Higher ...
16:45 - 17:07
CPP
Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust
17:07 - 17:30