Dortoirs - PLMW @ POPL 2026

Venuele Couvent des Jacobins

Room nameDortoirs

Floor1

Room InformationNo extra information available

Program

This program is tentative and subject to change.

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

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 TalksPOPL Student Research Competition at Dortoirs

10:20 16m Poster		RESpecBench: Rigorous Evaluation of Specification Generation with Automated Verification POPL 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 POPL Student Research Competition Lukas Kebuladze Carnegie Mellon University Pre-print
10:53 16m Poster		Semantic Completeness of Higher-Order Probabilistic Separation Logics POPL Student Research Competition Puming Liu New York University Shanghai
11:10 16m Poster		Language Model for MPI POPL 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 POPL 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 POPL 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	KeynotePOPL Student 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

Hide past events

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Dortoirs	POPL Keynote																		POPL Program Analysis																																										POPL Quantum 1																										POPL Decision Procedures

Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change


Room	10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30
Dortoirs					POPL Student Research Competition SRC Talks																																												POPL Category Theory																										POPL Synthesis 2

Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Dortoirs	POPL Student Research Competition + POPL Keynote																		POPL Specification and Verification Methods																																										POPL Monads and Effects																										POPL Types 3

Hide past events

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
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


Room	10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45
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


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
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

Hide past events

Room information: Dortoirs

This program is tentative and subject to change.

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

POPL

POPL

POPL

POPL

Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

POPL Student Research Competition

POPL

POPL

Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

POPL Student Research Competition + POPL

POPL

POPL

POPL

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Tracks

Room information: Dortoirs

This program is tentative and subject to change.

Program Display Configuration

Wed 14 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Thu 15 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Fri 16 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Wed 14 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

POPL

POPL

POPL

POPL

Thu 15 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

POPL Student Research Competition

POPL

POPL

Fri 16 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

POPL Student Research Competition + POPL

POPL

POPL

POPL

Wed 14 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Thu 15 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Fri 16 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Wed 14 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Thu 15 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change