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

Room information: Nef

Venuele Couvent des Jacobins
Room nameNef
Floor0
Capacity400
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

Wed 14 Jan

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

09:00 - 10:00
KeynotePOPL at Nef
09:00
60m
Keynote
Medium-scale automation for proof assistants
POPL
Damien Pous CNRS
10:30 - 12:10
Functional Programming POPL at Nef
10:30
25m
Talk
Domain-Theoretic Semantics for Functional Logic Programming
POPL
Eddie Jones University of Bristol, Samson Main University of Bristol, Celia Mengyue Li University of Bristol, Jonathan Marriott University of Bristol, Alex Kavvos University of Bristol
DOI
10:55
25m
Talk
Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks
POPL
Michael Lee University of Cambridge, UK, Ningning Xie University of Toronto, Oleg Kiselyov Tohoku University, Jeremy Yallop University of Cambridge
DOI
11:20
25m
Talk
Hyperfunctions: Communicating Continuations
POPL
Donnacha Oisín Kidney Imperial College London, Nicolas Wu Imperial College London
DOI Pre-print
11:45
25m
Talk
Lazy Linearity for a Core Functional Language
POPL
Rodrigo Mesquita Well-Typed LLP, Bernardo Toninho Instituto Superior Técnico - University of Lisbon
DOI Pre-print
14:00 - 15:40
Types 1POPL at Nef
14:00
25m
Talk
Extensible Data Types with Ad-Hoc Polymorphism
POPL
Matthew Toohey University of Toronto, Yanning Chen University of Toronto, Ara Jamalzadeh University of Toronto, Ningning Xie University of Toronto
DOI
14:25
25m
Talk
Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems
POPL
Joseph Zullo Purdue University
DOI
14:50
25m
Talk
Local Contextual Type Inference
POPL
Xu Xue University of Hong Kong, Chen Cui University of Hong Kong, Shengyi Jiang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI
15:15
25m
Talk
Typing Strictness
POPL
Daniel Sainati University of Pennsylvania, Joseph W. Cutler University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Stephanie Weirich University of Pennsylvania
DOI
16:10 - 17:25
Synthesis 1POPL at Nef
16:10
25m
Talk
Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages
POPL
Zhentao Ye Peking University, Ruyi Ji Peking University, Yingfei Xiong Peking University, Xin Zhang Peking University
DOI
16:35
25m
Talk
Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling
POPL
Doyoon Lee Seoul National University, Woosuk Lee Hanyang University, Kwangkeun Yi Seoul National University
DOI
17:00
25m
Talk
Oriented Metrics for Bottom-Up Enumerative Synthesis
POPL
Roland Meyer TU Braunschweig, Jakob Tepe TU Braunschweig
DOI

Thu 15 Jan

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

10:20 - 12:00
Concurrency: Testing and VerificationPOPL at Nef
10:20
25m
Talk
(TOPLAS) Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection
POPL
Alexandre Moine New York University, Arthur Charguéraud Inria, François Pottier Inria
10:45
25m
Talk
Verifying Almost-Sure Termination for Randomized Distributed Algorithms
POPL
Constantin Enea LIX, CNRS, Ecole Polytechnique, Rupak Majumdar MPI-SWS, Harshit Jitendra Motwani MPI-SWS, V.R. Sathiyanarayana MPI-SWS
DOI
11:10
25m
Talk
Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic
POPL
Clément Allain INRIA, Gabriel Scherer Université Paris Cité - Inria - CNRS
DOI
11:35
25m
Talk
The Complexity of Testing Message-Passing Concurrency
POPL
Zheng Shi National University of Singapore, Lasse Møldrup Aarhus University, Umang Mathur National University of Singapore, Andreas Pavlogiannis Aarhus University
DOI Pre-print
14:00 - 15:40
Proof AssistantsPOPL at Nef
14:00
25m
Talk
A Lazy, Concurrent Convertibility Checker
POPL
Nathanaëlle Courant OCamlPro, Xavier Leroy Collège de France - PSL University
DOI
14:25
25m
Talk
Canonicity for Indexed Inductive-Recursive Types
POPL
András Kovács University of Gothenburg and Chalmers University of Technology
DOI
14:50
25m
Talk
Coco: Corecursion with Compositional Heterogeneous Productivity
POPL
Jaewoo Kim Seoul National University, Yeonwoo Nam Seoul National University, Chung-Kil Hur Seoul National University
DOI
15:15
25m
Talk
Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation
POPL
Marcus Rossel Barkhausen Institut; TU Darmstadt, Rudi Schneider TU Berlin, Thomas Koehler ICube Lab - CNRS - Université de Strasbourg, Michel Steuwer TU Berlin, Andrés Goens TU Darmstadt
DOI
16:10 - 17:00
Verified CompilationPOPL at Nef
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

Fri 16 Jan

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

09:00 - 10:00
KeynoteStudent Research Competition / POPL at Nef
09:00
60m
Keynote
Hardware-Software Contracts for High Assurance with Applications to Side-Channel Security
POPL
Caroline Trippel Stanford University
10:30 - 12:10
Concurrency: Types, Logics, and LibrariesPOPL at Nef
10:30
25m
Talk
All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs
POPL
Alexandre Moine New York University, Sam Westrick New York University, Joseph Tassarotti New York University
DOI
10:55
25m
Talk
A Verified High-Performance Composable Object Library for Remote Direct Memory Access
POPL
Guillaume Ambal , George Hodgkins University of Colorado, Mark Madler University of Colorado, Gregory Chockler University of Surrey, Brijesh Dongol University of Surrey, Joe Izraelevitz University of Colorodo Boulder, Azalea Raad Imperial College London, Viktor Vafeiadis MPI-SWS
DOI
11:20
25m
Talk
DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
POPL
Aleksandr Fedchin Tufts University, Antero Mejr Tufts University, Hari Sundar Tufts University, Jeffrey S. Foster Tufts University
DOI
11:45
25m
Talk
TypeDis: A Type System for Disentanglement
POPL
Alexandre Moine New York University, Stephanie Balzer Carnegie Mellon University, Alex Xu Carnegie Mellon University, Sam Westrick New York University
DOI
14:00 - 15:40
Probabilistic ProgrammingPOPL at Nef
14:00
25m
Talk
Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
POPL
Sangho Lim KAIST, Hyoungjin Lim KAIST, Wonyeol Lee POSTECH, Xavier Rival Inria - CNRS - Ecole Normale Superieure de Paris - PSL University, Hongseok Yang KAIST
DOI
14:25
25m
Talk
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
POPL
Noam Zilberstein Cornell University, Alexandra Silva Cornell University, Joseph Tassarotti New York University
DOI
14:50
25m
Talk
Probabilistic Programming with Vectorized Programmable Inference
POPL
McCoy Reynolds Becker MIT, Mathieu Huot MIT, George Matheos Massachusetts Institute of Technology, Xiaoyan Wang Massachusetts Institute of Technology, Karen Chung Massachusetts Institute of Technology, Colin Smith Massachusetts Institute of Technology, Sam Ritchie Massachusetts Institute of Technology, Rif A. Saurous Google, Alexander K. Lew Yale University, Martin C. Rinard Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology
DOI
15:15
25m
Talk
Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages
POPL
Davide Barbarossa University of Bath, Paolo Pistone Université Claude Bernard Lyon 1
DOI
16:10 - 17:25
Automata 2POPL at Nef
16:10
25m
Talk
Counting and Sampling Traces in Regular Languages
POPL
Alexis de Colnet TU Wien, Kuldeep S. Meel University of Toronto, Umang Mathur National University of Singapore
DOI Pre-print
16:35
25m
Talk
Parametrised Verification of Intel-x86 Programs
POPL
Parosh Aziz Abdulla Uppsala University; Mälardalen University, Mohamed Faouzi Atig Uppsala University, Ahmed Bouajjani Université Paris Cité, K Narayan Kumar Chennai Mathematical Institute, Prakash Saivasan Institute of Mathematical Sciences
DOI
17:00
25m
Talk
General Decidability Results for Systems with Continuous Counters
POPL
A. R. Balasubramanian Technical University of Munich, Matthew Hague Royal Holloway University of London, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Uppsala University, Georg Zetzsche MPI-SWS
DOI

Wed 14 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Nef

POPL

Keynote

POPL

Functional Programming

POPL

Types 1

POPL

Synthesis 1

Thu 15 Jan

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

Room10:003011:003012:003013:003014:003015:003016:003017:0030
Nef

POPL

Concurrency: Testing and Verification

POPL

Proof Assistants

POPL

Verified Compilation

POPL

Fri 16 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Nef

Student Research Competition + POPL

Keynote

POPL

Concurrency: Types, Logics, and Libraries

POPL

Probabilistic Programming

POPL

Automata 2

Wed 14 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Nef
POPL
Medium-scale automation for proof assistants
09:00 - 10:00
POPL
Domain-Theoretic Semantics for Functional Logic Programming
10:30 - 10:55
POPL
Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrus ...
10:55 - 11:20
POPL
Hyperfunctions: Communicating Continuations
11:20 - 11:45
POPL
Lazy Linearity for a Core Functional Language
11:45 - 12:10
POPL
Extensible Data Types with Ad-Hoc Polymorphism
14:00 - 14:25
POPL
Let Generalization, Polymorphic Recursion, and Variable Minimization in ...
14:25 - 14:50
POPL
Local Contextual Type Inference
14:50 - 15:15
POPL
Typing Strictness
15:15 - 15:40
POPL
Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Speci ...
16:10 - 16:35
POPL
Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling
16:35 - 17:00
POPL
Oriented Metrics for Bottom-Up Enumerative Synthesis
17:00 - 17:25

Thu 15 Jan

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

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:00153045
Nef
POPL
(TOPLAS) Will it Fit? Verifying Heap Space Bounds of Concurrent Progra ...
10:20 - 10:45
POPL
Verifying Almost-Sure Termination for Randomized Distributed Algorithms
10:45 - 11:10
POPL
Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs us ...
11:10 - 11:35
POPL
The Complexity of Testing Message-Passing Concurrency
11:35 - 12:00
POPL
A Lazy, Concurrent Convertibility Checker
14:00 - 14:25
POPL
Canonicity for Indexed Inductive-Recursive Types
14:25 - 14:50
POPL
Coco: Corecursion with Compositional Heterogeneous Productivity
14:50 - 15:15
POPL
Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem ...
15:15 - 15:40
POPL
A Family of Sims with Diverging Interests
16:10 - 16:35
POPL
Endangered by the Language But Saved by the Compiler: Robust Safety via ...
16:35 - 17:00

Fri 16 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Nef
POPL
Hardware-Software Contracts for High Assurance with Applications to Sid ...
09:00 - 10:00
POPL
All for One and One for All: Program Logics for Exploiting Internal Det ...
10:30 - 10:55
POPL
A Verified High-Performance Composable Object Library for Remote Direct ...
10:55 - 11:20
POPL
DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
11:20 - 11:45
POPL
TypeDis: A Type System for Disentanglement
11:45 - 12:10
POPL
Optimising Density Computations in Probabilistic Programs via Automatic ...
14:00 - 14:25
POPL
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Cond ...
14:25 - 14:50
POPL
Probabilistic Programming with Vectorized Programmable Inference
14:50 - 15:15
POPL
Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of P ...
15:15 - 15:40
POPL
Counting and Sampling Traces in Regular Languages
16:10 - 16:35
POPL
Parametrised Verification of Intel-x86 Programs
16:35 - 17:00
POPL
General Decidability Results for Systems with Continuous Counters
17:00 - 17:25