Program - POPL 2026

Detailed Table Session Timeline Detailed Timeline

Time Zone

The program is currently displayed in (GMT+01:00) Brussels, Copenhagen, Madrid, Paris.

Use conference time zone: (GMT+01:00) Brussels, Copenhagen, Madrid, ParisSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

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		How can Machine Learning Help Formal Proving ? CPP K: Amaury Hayat Ecole nationale des Ponts et Chaussées
10:08 22m Talk		Higher order differential calculus in Mathlibdistinguished paper 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 Chair(s): Sophie Tourret Inria and Max Planck Institute for Informatics

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 Chair(s): Matthieu Sozeau Inria

16:00 22m Talk		Mechanized Dominator Tree Certificationdistinguished paper CPP Jean-Christophe Léchenet Université Côte d’Azur, Inria DOI Pre-print
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 NTU Singapore, 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		Specification, Semantics, and Verification of Quantum Programs 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 Chair(s): Cyril Cohen Inria, CNRS, ENS Lyon, UCBL, LIP

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 DOI Pre-print
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 DOI
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

14:00 - 15:30	Program verificationCPP at Belvédère Chair(s): Clement Pit-Claudel EPFL

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 Pre-print
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:50	Separation logicCPP at Belvédère Chair(s): Thibault Dardinier EPFL

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 Pinningdistinguished paper CPP Yawen Guan EPFL, Clément Pit-Claudel EPFL DOI Pre-print
16:44 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:06 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 LMF, CNRS, Université Paris-Saclay
17:28 22m Talk		A Rose Tree is Blooming (Proof Pearl) CPP Joomy Korkut Bloomberg DOI Pre-print

CPP 2026 Program

Mon 12 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Tue 13 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

CPP 2026 Program

Switch Program View

Program Display Configuration

Mon 12 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Tue 13 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Get Calendar (iCal)

Mon 12 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Tue 13 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change