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

Room information: Dortoirs

Venuele Couvent des Jacobins
Room nameDortoirs
Floor1
Room InformationNo extra information available
Program

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 Dortoirs
09:00
60m
Keynote
Medium-scale automation for proof assistants
POPL
Damien Pous CNRS
10:30 - 12:10
Program AnalysisPOPL at Dortoirs
Chair(s): Xavier Rival Inria - CNRS - Ecole Normale Superieure de Paris - PSL University
10:30
25m
Talk
A Modular Static Cost Analysis for GPU Warp-Level Parallelism
POPL
Gregory Blike University of Massachusetts at Boston, Hannah Zicarelli University of Massachusetts at Boston, Udaya Sathiyamoorthy University of Massachusetts at Boston, Julien Lange Royal Holloway University of London, Tiago Cogumbreiro University of Massachusetts at Boston
DOI
10:55
25m
Talk
ChiSA: Static Analysis for Lightweight Chisel Verification
POPL
Jiacai Cui Nanjing University, Qinlin Chen Nanjing University, Zhongsheng Zhan Nanjing University, Tian Tan Nanjing University, Yue Li Nanjing University
DOI
11:20
25m
Talk
Miri: Practical Undefined Behavior Detection for Rust
POPL
Ralf Jung ETH Zurich, Benjamin Kimock Lansweeper NV, Christian Poveda Unaffiliated, Eduardo Sánchez Muñoz Unaffiliated, Oli Scherer Unaffiliated, Qian (Andy) Wang ETH Zurich and Imperial College London
DOI
11:45
25m
Talk
Piecewise Analysis of Probabilistic Programs via k-Induction
POPL
Tengshun Yang Institute of Software at Chinese Academy of Sciences, Shenghua Feng Institute of Software at Chinese Academy of Sciences, Hongfei Fu Shanghai Jiao Tong University, Naijun Zhan Peking University; Zhongguancun Lab, Jingyu Ke Shanghai Jiao Tong University, Shiyang Wu Shanghai Jiao Tong University
DOI
14:00 - 15:40
Quantum 1POPL at Dortoirs
Chair(s): Ugo Dal Lago University of Bologna; Centre Inria d’Université Côte d’Azur
14:00
25m
Talk
An Expressive Assertion Language for Quantum Programs
POPL
Bonan Su Tsinghua University, Yuan Feng Tsinghua University, Mingsheng Ying Institute of Software at Chinese Academy of Sciences; Tsinghua University, Li Zhou Institute of Software at Chinese Academy of Sciences
DOI
14:25
25m
Talk
Hadamard-Pi: Equational Quantum Programming
POPL
Wang Fang University of Edinburgh, Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark
DOI
14:50
25m
Talk
Qudit Quantum Programming with Projective Cliffords
POPL
Jennifer Paykin University of Vermont, Sam Winnick Simon Fraser University; University of Waterloo
DOI
15:15
25m
Talk
RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
POPL
Yusuke Matsushita Kyoto University, Kengo Hirata University of Edinburgh, Ryo Wakizaka Kyoto University, Emanuele D'Osualdo University of Konstanz
DOI Pre-print
16:10 - 17:25
Decision ProceduresPOPL at Dortoirs
Chair(s): Andrés Goens TU Darmstadt
16:10
25m
Talk
Characterizing Sets of Theories That Can Be Disjointly Combined
POPL
Benjamin Przybocki Carnegie Mellon University, Guilherme V. Toledo Bar-Ilan University, Yoni Zohar
DOI
16:35
25m
Talk
Context-Free-Language Reachability for Almost-Commuting Transition Systems
POPL
Nikhil Pimpalkhare Princeton University, Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin-Madison
DOI
17:00
25m
Talk
Determination Problems for Orbit Closures and Matrix Groups
POPL
Rida Ait El Manssour University of Oxford, George Kenison Liverpool John Moores University, Mahsa Shirmohammadi CNRS, Anton Varonka TU Wien, James Worrell University of Oxford
DOI

Thu 15 Jan

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

10:20 - 12:00
SRC TalksStudent Research Competition at Dortoirs
10:20
16m
Poster
RESpecBench: Rigorous Evaluation of Specification Generation with Automated Verification
Student Research Competition
Barış Bayazıt University of Toronto, Xujie Si University of Toronto
10:36
16m
Poster
Amortized Analysis of Splay Trees via a Lax Homomorphism
Student Research Competition
Lukas Kebuladze Carnegie Mellon University
Pre-print
10:53
16m
Poster
Semantic Completeness of Higher-Order Probabilistic Separation Logics
Student Research Competition
Puming Liu New York University Shanghai
11:10
16m
Poster
Language Model for MPI
Student Research Competition
Keith Allen University at Buffalo, SUNY, Andrew K. Hirsch University at Buffalo, SUNY
11:26
16m
Poster
Bootstrapping a Verified Compiler for an Imperative Language in Rocq
Student Research Competition
Kacper F. Korban EPFL
11:43
16m
Poster
An End-to-end Theory for Compositional Symbolic Execution: From Expressive Specifications to SMT
Student Research Competition
Shivanandan Tamil Kumaran Imperial College London
14:00 - 15:40
Category TheoryPOPL at Dortoirs
Chair(s): Kenji Maillard Inria
14:00
25m
Talk
Classical Notions of Computation and the Hasegawa-Thielecke Theorem
POPL
Éléonore Mangel Univ. Paris Cité - CNRS - Inria, Paul-André Melliès Univ. Paris Cité - CNRS - Inria, Guillaume Munch-Maccagnoni INRIA
DOI
14:25
25m
Talk
From Semantics to Syntax: A Type Theory for Comprehension Categories
POPL
Niyousha Najmaei École Polytechnique, Niels van der Weide Radboud University, Benedikt Ahrens Delft University of Technology, Paige Randall North Utrecht University
DOI
14:50
25m
Talk
Higher-Order Behavioural Conformances via Fibrations
POPL
Henning Urbat Friedrich-Alexander-University Erlangen-Nürnberg
DOI
15:15
25m
Talk
What Is a Monoid?
POPL
Paul Blain Levy University of Birmingham, Morgan Rogers University Sorbonne Paris 13
DOI
16:10 - 17:00
Synthesis 2POPL at Dortoirs
Chair(s): Marco Campion Inria Paris - ENS - Université PSL
16:10
25m
Talk
Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
POPL
Xuanyu Peng University of California at San Diego, Dominic Kennedy University of Utah, Yuyou Fan University of Utah, Ben Greenman University of Utah, USA, John Regehr University of Utah, Loris D'Antoni University of California at San Diego
DOI
16:35
25m
Talk
Parameterized Infinite-State Reactive Synthesis
POPL
Benedikt Maderbacher Graz University of Technology, Roderick Bloem Graz University of Technology
DOI

Fri 16 Jan

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

09:00 - 10:00
KeynoteStudent Research Competition / POPL at Dortoirs
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
Specification and Verification MethodsPOPL at Dortoirs
Chair(s): Ben Greenman University of Utah, USA
10:30
25m
Talk
Abstraction Functions as Types
POPL
Harrison Grodin Carnegie Mellon University, Runming Li Carnegie Mellon University, Robert Harper Carnegie Mellon University
DOI
10:55
25m
Talk
Foundational Multi-Modal Program Verifiers
POPL
Vladimir Gladshtein , George Pîrlea National University of Singapore, Qiyuan Zhao National University of Singapore, Vitaly Kurin Neapolis University Pafos, Ilya Sergey National University of Singapore
DOI
11:20
25m
Talk
Stateful Differential Operators for Incremental Computing
POPL
Runqing Xu KIT, Sebastian Erdweg KIT
DOI
11:45
25m
Talk
The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs
POPL
Frank Schüssele University of Freiburg, Matthias Zumkeller University of Freiburg, Miriam Lagunes-Rochin University of Freiburg, Dominik Klumpp LIX - CNRS - École Polytechnique; University of Freiburg
DOI
14:00 - 15:40
Monads and EffectsPOPL at Dortoirs
Chair(s): Henning Urbat Friedrich-Alexander-University Erlangen-Nürnberg
14:00
25m
Talk
An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic TheoriesDistinguished Paper
POPL
Ohad Kammar University of Edinburgh, Jack Liell-Cock University of Oxford, Sam Lindley University of Edinburgh, Cristina Matache University of Edinburgh, Sam Staton University of Oxford
DOI
14:25
25m
Talk
Handling Higher-Order Effectful Operations with Judgemental Monadic Laws
POPL
Zhixuan Yang Imperial College London, Nicolas Wu Imperial College London
DOI
14:50
25m
Talk
Rows and Capabilities as Modal Effects
POPL
Wenhao Tang The University of Edinburgh, Sam Lindley University of Edinburgh
DOI
15:15
25m
Talk
The Relative Monadic Metalanguage
POPL
Jack Liell-Cock University of Oxford, Zev Shirazi University of Oxford, Sam Staton University of Oxford
DOI
16:10 - 17:25
Types 3POPL at Dortoirs
Chair(s): Nicolas Wu Imperial College London
16:10
25m
Talk
A Complementary Approach to Incorrectness Typing
POPL
Celia Mengyue Li University of Bristol, Sophie Pull University of Bristol, Steven Ramsay University of Bristol
DOI
16:35
25m
Talk
A Synthetic Reconstruction of Multiparty Session Types
POPL
David Castro-Perez University of Kent, Francisco Ferreira Royal Holloway, University of London, Sung-Shik Jongmans University of Groningen
DOI
17:00
25m
Talk
Bounded Sort Polymorphism with Elimination Constraints
POPL
Johann Rosain ENS Lyon, Tomás Diaz University of Chile, Kenji Maillard Inria, Matthieu Sozeau Inria, Nicolas Tabareau Inria, Éric Tanter University of Chile, Théo Winterhalter INRIA
DOI

Wed 14 Jan

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

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

POPL

Keynote

POPL

Program Analysis

POPL

Quantum 1

POPL

Decision Procedures

Thu 15 Jan

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

Room10:003011:003012:003013:003014:003015:003016:0030
Dortoirs

Student Research Competition

SRC Talks

POPL

Category Theory

POPL

Synthesis 2

Fri 16 Jan

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

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

Student Research Competition + POPL

Keynote

POPL

Specification and Verification Methods

POPL

Monads and Effects

POPL

Types 3

Wed 14 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Dortoirs
POPL
Medium-scale automation for proof assistants
09:00 - 10:00
POPL
A Modular Static Cost Analysis for GPU Warp-Level Parallelism
10:30 - 10:55
POPL
ChiSA: Static Analysis for Lightweight Chisel Verification
10:55 - 11:20
POPL
Miri: Practical Undefined Behavior Detection for Rust
11:20 - 11:45
POPL
Piecewise Analysis of Probabilistic Programs via k-Induction
11:45 - 12:10
POPL
An Expressive Assertion Language for Quantum Programs
14:00 - 14:25
POPL
Hadamard-Pi: Equational Quantum Programming
14:25 - 14:50
POPL
Qudit Quantum Programming with Projective Cliffords
14:50 - 15:15
POPL
RapunSL: Untangling Quantum Computing with Separation, Linear Combinati ...
15:15 - 15:40
POPL
Characterizing Sets of Theories That Can Be Disjointly Combined
16:10 - 16:35
POPL
Context-Free-Language Reachability for Almost-Commuting Transition Systems
16:35 - 17:00
POPL
Determination Problems for Orbit Closures and Matrix Groups
17:00 - 17:25

Thu 15 Jan

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

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:00153045
Dortoirs
POPL Student Research Competition
RESpecBench: Rigorous Evaluation of Specification Generation with Autom ...
10:20 - 10:36
POPL Student Research Competition
Amortized Analysis of Splay Trees via a Lax Homomorphism
10:36 - 10:53
POPL Student Research Competition
Semantic Completeness of Higher-Order Probabilistic Separation Logics
10:53 - 11:10
POPL Student Research Competition
Language Model for MPI
11:10 - 11:26
POPL Student Research Competition
Bootstrapping a Verified Compiler for an Imperative Language in Rocq
11:26 - 11:43
POPL Student Research Competition
An End-to-end Theory for Compositional Symbolic Execution: From Express ...
11:43 - 12:00
POPL
Classical Notions of Computation and the Hasegawa-Thielecke Theorem
14:00 - 14:25
POPL
From Semantics to Syntax: A Type Theory for Comprehension Categories
14:25 - 14:50
POPL
Higher-Order Behavioural Conformances via Fibrations
14:50 - 15:15
POPL
What Is a Monoid?
15:15 - 15:40
POPL
Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
16:10 - 16:35
POPL
Parameterized Infinite-State Reactive Synthesis
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
Dortoirs
POPL
Hardware-Software Contracts for High Assurance with Applications to Sid ...
09:00 - 10:00
POPL
Abstraction Functions as Types
10:30 - 10:55
POPL
Foundational Multi-Modal Program Verifiers
10:55 - 11:20
POPL
Stateful Differential Operators for Incremental Computing
11:20 - 11:45
POPL
The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs
11:45 - 12:10
POPL Distinguished Paper
An Equational Axiomatization of Dynamic Threads via Algebraic Effects: ...
14:00 - 14:25
POPL
Handling Higher-Order Effectful Operations with Judgemental Monadic Laws
14:25 - 14:50
POPL
Rows and Capabilities as Modal Effects
14:50 - 15:15
POPL
The Relative Monadic Metalanguage
15:15 - 15:40
POPL
A Complementary Approach to Incorrectness Typing
16:10 - 16:35
POPL
A Synthetic Reconstruction of Multiparty Session Types
16:35 - 17:00
POPL
Bounded Sort Polymorphism with Elimination Constraints
17:00 - 17:25