Réfectoire - POPL 2026

Venuele Couvent des Jacobins

Room nameRéfectoire

Floor0

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

10:30 - 12:10	Automata 1POPL at Réfectoire

10:30 25m Talk		Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures POPL C. Aiswarya Chennai Mathematical Institute, Pascal Baumann MPI-SWS, Prakash Saivasan Institute of Mathematical Sciences, Lia Schütze MPI-SWS, Georg Zetzsche MPI-SWS DOI
10:55 25m Talk		Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications POPL Aurèle Barrière EPFL, Victor Deng EPFL; École Normale Supérieure - PSL - CNRS, Clément Pit-Claudel EPFL DOI
11:20 25m Talk		Network Change Validation with Relational NetKAT POPL Han Xu Princeton University, Zachary Kincaid Princeton University, Ratul Mahajan University of Washington, Intentionet, David Walker DOI
11:45 25m Talk		Parameterized Verification of Quantum Circuits POPL Parosh Aziz Abdulla Uppsala University; Mälardalen University, Yu-Fang Chen Academia Sinica, Michal Hečko Brno University of Technology, Lukáš Holík Brno University of Technology; Aalborg University, Ondřej Lengál Brno University of Technology, Jyun-Ao Lin National Taipei University of Technology, Ramanathan S. Thinniyam Uppsala University DOI

14:00 - 15:40	Concurrency: ModelsPOPL at Réfectoire

14:00 25m Talk		Arbitration-Free Consistency Is Available (and Vice Versa) POPL Hagit Attiya Technion - Israel Institute of Technology, Constantin Enea LIX, CNRS, Ecole Polytechnique, Enrique Román-Calvo University of Freiburg DOI
14:25 25m Talk		ArchSem: Reusable Rigorous Semantics of Relaxed Architectures POPL Thibaut Pérami University of Cambridge, Thomas Bauereiss University of Cambridge, Brian Campbell University of Edinburgh, Zongyuan Liu Aarhus University, Nils Lauermann University of Cambridge, Alasdair Armstrong University of Cambridge, Peter Sewell University of Cambridge DOI
14:50 25m Talk		Consistent Updates for Scalable Microservices POPL Devora Chait-Roth New York University, Kedar Namjoshi Nokia Bell Labs, Thomas Wies New York University DOI
15:15 25m Talk		Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models POPL Thomas Haas TU Braunschweig, Roland Meyer TU Braunschweig, Hernán Ponce de León Huawei Dresden Research Center, Andrés Lomelí Garduño Huawei Dresden Research Center DOI

16:10 - 17:25	Machine LearningPOPL at Réfectoire

16:10 25m Talk		ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models POPL Shaan Nagy University of California at San Diego, Timothy Zhou , Nadia Polikarpova University of California at San Diego, Loris D'Antoni University of California at San Diego DOI
16:35 25m Talk		Compiling to Linear Neurons POPL Joey Velez-Ginorio , Nada Amin Harvard University, Konrad Kording University of Pennsylvania, Steve Zdancewic University of Pennsylvania DOI
17:00 25m Talk		Fuzzing Guided by Bayesian Program Analysis POPL Yifan Zhang Peking University, Xin Zhang Peking University DOI

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

10:20 - 12:00	Separation LogicPOPL at Réfectoire

10:20 25m Talk		A Relational Separation Logic for Effect Handlers POPL Paulo Emílio de Vilhena Imperial College London, Simcha van Collem Radboud University Nijmegen, Ines Wright Aarhus University, Robbert Krebbers Radboud University Nijmegen DOI
10:45 25m Talk		Bayesian Separation Logic POPL Shing Hin Ho Imperial College London, Nicolas Wu Imperial College London, Azalea Raad Imperial College London DOI Pre-print
11:10 25m Talk		Cryptis: Cryptographic Reasoning in Separation Logic POPL Arthur Azevedo de Amorim Rochester Institute of Technology, Amal Ahmed Northeastern University, USA, Marco Gaboardi Boston University DOI
11:35 25m Talk		Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions POPL Neta Elad Tel Aviv University, Adithya Murali University of Wisconsin, Sharon Shoham Tel Aviv University DOI

14:00 - 15:40	Program Logics and Semantic FrameworksPOPL at Réfectoire

14:00 25m Talk		A Logic for the Imprecision of Abstract Interpretations POPL Marco Campion Inria Paris - ENS - Université PSL, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Arizona, Caterina Urban Inria Paris - ENS - Université PSL DOI
14:25 25m Talk		Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment POPL David M. Kahn Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University, Runming Li Carnegie Mellon University DOI
14:50 25m Talk		JAX Autodiff from a Linear Logic Perspective POPL Giulia Giusti ENS Lyon, Michele Pagani ENS Lyon DOI
15:15 25m Talk		U-Turn: Enhancing Incorrectness Analysis by Reversing Direction POPL Flavio Ascari University of Konstanz, Roberto Bruni University of Pisa, Roberta Gori Diaprtimento di Informatica, Universita' di Pisa, Italy, Azalea Raad Imperial College London DOI

16:10 - 17:00	Security and PrivacyPOPL at Réfectoire

16:10 25m Talk		Dependent Coeffects for Local Sensitivity Analysis POPL Victor Sannier Univ. Lille - CNRS - Inria - Centrale Lille - UMR 9189 CRIStAL, Patrick Baillot Univ. Lille - CNRS - Inria - Centrale Lille - UMR 9189 CRIStAL DOI
16:35 25m Talk		Security Reasoning via Substructural Dependency Tracking POPL Hemant Gouni Carnegie Mellon University, Frank Pfenning Carnegie Mellon University, USA, Jonathan Aldrich Carnegie Mellon University DOI Pre-print

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

10:30 - 12:10	Types 2POPL at Réfectoire

10:30 25m Talk		Di- is for Directed: First-Order Directed Type Theory via Dinaturality POPL Andrea Laretto Tallinn University of Technology, Fosco Loregian Tallinn University of Technology, Niccolò Veltri IT University of Copenhagen DOI
10:55 25m Talk		Quotient Polymorphism POPL Brandon Hewer , Graham Hutton University of Nottingham DOI
11:20 25m Talk		The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types POPL Chun Yin Chau HKUST (The Hong Kong University of Science and Technology), Lionel Parreaux Hong Kong University of Science and Technology DOI
11:45 25m Talk		Welterweight Go: Boxing, Structural Subtyping, and Generics POPL Raymond Hu Queen Mary University of London, Julien Lange Royal Holloway University of London, Bernardo Toninho Instituto Superior Técnico - University of Lisbon, Philip Wadler University of Edinburgh, Robert Griesemer Google, Keith Randall Google DOI

14:00 - 15:40	Proof Assistants 2POPL at Réfectoire

14:00 25m Talk		AdapTT: Functoriality for Dependent Type Casts POPL Arthur Adjedj ENS Paris Saclay, Université Paris-Saclay, Meven Lennon-Bertrand Inria – Université Paris Cité, Thibaut Benjamin Université Paris-Saclay, CEA, List, Kenji Maillard Inria DOI
14:25 25m Talk		Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach POPL Yiyun Liu University of Pennsylvania, Stephanie Weirich University of Pennsylvania DOI
14:50 25m Talk		Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally POPL Yann Leray Nantes Université; Inria, Théo Winterhalter INRIA DOI
15:15 25m Talk		Normalisation for First-Class Universe Levels POPL Nils Anders Danielsson University of Gothenburg, Naïm Camille Favier Chalmers University of Technology and University of Gothenburg, Ondřej Kubánek Chalmers University of Technology DOI

16:10 - 17:25	Quantum 2POPL at Réfectoire

16:10 25m Talk		Generating Compilers for Qubit Mapping and Routing POPL Abtin Molavi University of Wisconsin-Madison, Amanda Xu University of Wisconsin-Madison, Ethan Cecchetti University of Wisconsin-Madison, Swamit Tannu University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison DOI
16:35 25m Talk		On Circuit Description Languages, Indexed Monads, and Resource Analysis POPL Ken Sakayori University of Tokyo, Andrea Colledan University of Bologna; Centre Inria d’Université Côte d’Azur, Ugo Dal Lago University of Bologna; Centre Inria d’Université Côte d’Azur DOI
17:00 25m Talk		Quantum Circuits Are Just a Phase POPL Chris Heunen University of Edinburgh, Louis Lemonnier University of Edinburgh, Christopher McNally Massachusetts Institute of Technology, Alex Rice University of Edinburgh DOI

Wed 14 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						17:00						30
Réfectoire							POPL Automata 1																																										POPL Concurrency: Models																										POPL Machine Learning

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
Réfectoire					POPL Separation Logic																																												POPL Program Logics and Semantic Frameworks																										POPL Security and Privacy

Fri 16 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						17:00						30
Réfectoire							POPL Types 2																																										POPL Proof Assistants 2																										POPL Quantum 2

Wed 14 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			17:00			15			30			45
Réfectoire							POPL Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures 10:30 - 10:55					POPL Formal Verification for JavaScript Regular Expressions: A Proven Mechan ... 10:55 - 11:20					POPL Network Change Validation with Relational NetKAT 11:20 - 11:45					POPL Parameterized Verification of Quantum Circuits 11:45 - 12:10																											POPL Arbitration-Free Consistency Is Available (and Vice Versa) 14:00 - 14:25					POPL ArchSem: Reusable Rigorous Semantics of Relaxed Architectures 14:25 - 14:50					POPL Consistent Updates for Scalable Microservices 14:50 - 15:15					POPL Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory ... 15:15 - 15:40											POPL ChopChop: A Programmable Framework for Semantically Constraining the Ou ... 16:10 - 16:35					POPL Compiling to Linear Neurons 16:35 - 17:00					POPL Fuzzing Guided by Bayesian Program Analysis 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
Réfectoire					POPL A Relational Separation Logic for Effect Handlers 10:20 - 10:45					POPL Bayesian Separation Logic 10:45 - 11:10					POPL Cryptis: Cryptographic Reasoning in Separation Logic 11:10 - 11:35					POPL Separating the Wheat from the Chaff: Understanding (In-)Completeness of ... 11:35 - 12:00																													POPL A Logic for the Imprecision of Abstract Interpretations 14:00 - 14:25					POPL Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment 14:25 - 14:50					POPL JAX Autodiff from a Linear Logic Perspective 14:50 - 15:15					POPL U-Turn: Enhancing Incorrectness Analysis by Reversing Direction 15:15 - 15:40											POPL Dependent Coeffects for Local Sensitivity Analysis 16:10 - 16:35					POPL Security Reasoning via Substructural Dependency Tracking 16:35 - 17:00

Fri 16 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			17:00			15			30			45
Réfectoire							POPL Di- is for Directed: First-Order Directed Type Theory via Dinaturality 10:30 - 10:55					POPL Quotient Polymorphism 10:55 - 11:20					POPL The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness f ... 11:20 - 11:45					POPL Welterweight Go: Boxing, Structural Subtyping, and Generics 11:45 - 12:10																											POPL AdapTT: Functoriality for Dependent Type Casts 14:00 - 14:25					POPL Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped ... 14:25 - 14:50					POPL Encode the Cake and Eat It Too: Controlling Computation in Type Theory, ... 14:50 - 15:15					POPL Normalisation for First-Class Universe Levels 15:15 - 15:40											POPL Generating Compilers for Qubit Mapping and Routing 16:10 - 16:35					POPL On Circuit Description Languages, Indexed Monads, and Resource Analysis 16:35 - 17:00					POPL Quantum Circuits Are Just a Phase 17:00 - 17:25

Room information: Réfectoire

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

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

POPL

POPL

POPL

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

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

Co-hosted Conferences

Workshops

Co-hosted Symposia

Room information: Réfectoire

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

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

POPL

POPL

POPL

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

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