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

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

10:30 - 12:10
Program AnalysisPOPL at Dortoirs
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
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
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 TalksPOPL at Dortoirs
14:00 - 15:40
Category TheoryPOPL at Dortoirs
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 - LS2N - CNRS
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
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

10:30 - 12:10
Specification and Verification MethodsPOPL at Dortoirs
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
14:00
25m
Talk
An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories
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
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

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

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

POPL

SRC Talks

POPL

Category Theory

POPL

Synthesis 2

Fri 16 Jan

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

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

POPL

Specification and Verification Methods

POPL

Monads and Effects

POPL

Types 3

Wed 14 Jan

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

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Dortoirs
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

Room14:0015304515:0015304516:00153045
Dortoirs
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

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Dortoirs
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
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