Salle 13 - POPL 2026

Venuele Couvent des Jacobins

Room nameSalle 13

Floor1

Room InformationNo extra information available

Program

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

Sun 11 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

09:00 - 10:30	First SessionLAFI at Salle 13 Chair(s): Alexander K. Lew Yale University

09:00 5m Day opening		Welcome LAFI Hugo Paquet Inria, École Normale Supérieure, Alexander K. Lew Yale University
09:07 20m Industry talk		Basis — A Programming Languages Take on Principled Foundations for AI LAFI Kiran Gopinathan Basis
09:29 10m Talk		Towards an Equational Calculus of Interventions LAFI Shubh Agrawal Northeastern University, Jialu Bao Northeastern University, Steven Holtzen Northeastern University Pre-print
09:41 10m Talk		Typed Abstractions for Causal Probabilistic Programming LAFI Theo Wang University of Cambridge, University of Oxford, Dario Stein University of Oxford, Eli Bingham Broad Institute, Jack Feser Basis, Ohad Kammar University of Edinburgh, Michael Lee University of Cambridge, UK, Jeremy Yallop University of Cambridge File Attached
09:53 10m Talk		A Design for Massively Parallel Gibbs Sampling on the GPU via Static and Dynamic Analysis of Probabilistic Programs LAFI Matin Ghavami Massachusetts Institute of Technology, Martin C. Rinard Massachusetts Institute of Technology, Vikash Mansinghka Massachusetts Institute of Technology
10:05 10m Talk		A Design Proposal for GraPPL: Probabilistic Programming with Low-Level, High-Performance GPU Programmable Inference LAFI Karen Chung Massachusetts Institute of Technology, Elias Rojas Collins MIT, McCoy Reynolds Becker MIT, Mathieu Huot MIT, Vikash Mansinghka Massachusetts Institute of Technology

11:00 - 12:30	Second SessionLAFI at Salle 13 Chair(s): Hugo Paquet Inria, École Normale Supérieure

11:00 55m Keynote		A Welcome to Causal Probabilistic Programming LAFI Dario Stein
11:56 10m Talk		Verifying Sampling Algorithms via Distributional Invariants LAFI Daniel Zilken , Tobias Winkler RWTH Aachen University, Kevin Batz RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University Media Attached File Attached
12:08 10m Talk		Sequential Monte Carlo Program Synthesis with Refinement Proposals LAFI Maddy Bowers Massachusetts Institute of Technology, Mauricio Barba da Costa MIT, Xiaoyan Wang Massachusetts Institute of Technology, Joshua B. Tenenbaum Massachusetts Institute of Technology, Vikash Mansinghka Massachusetts Institute of Technology, Armando Solar-Lezama Massachusetts Institute of Technology, Alexander K. Lew Yale University
12:20 10m Talk		A Word Sampler for Well-Typed Functions LAFI Breandan Considine Pre-print File Attached

14:00 - 15:30	Third SessionLAFI at Salle 13 Chair(s): Cameron Freer Massachusetts Institute of Technology

14:00 10m Talk		Towards Compiling Higher-Order Programs to Bayesian Networks LAFI Claudia Faggian CNRS, Université Paris Cité, Gabriele Vanoni IRIF, Université Paris Cité
14:12 10m Talk		On Contextual Distances in Randomized Programming: Amplification and Lower Bounds LAFI Houssein Mansour ISAE-SUPAERO, Raphaëlle Crubillé
14:24 10m Talk		Nominal Semantics for First-class Automatic Differentiation LAFI Jack Czenszak Yale University, Alexander K. Lew Yale University
14:36 10m Talk		Semantic Foundations for Laziness in Discrete Probabilistic Programming LAFI Simon Castellan University of Rennes; Inria; CNRS; IRISA, Tom Hirschowitz Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry, Hugo Paquet Inria, École Normale Supérieure
14:48 10m Talk		Incremental Density Computation for Efficient Programmable Inference LAFI Fabian Zaiser MIT, Vikash Mansinghka Massachusetts Institute of Technology, Alexander K. Lew Yale University
15:00 10m Talk		Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops LAFI Kevin Batz , Adrian Gallus RWTH Aachen University, Darion Haase RWTH Aachen University, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Lutz Klinkenberg RWTH Aachen University, Tobias Winkler RWTH Aachen University
15:12 10m Talk		Probabilistic Programming Meets Automata Theory: Exact Inference using Weighted Automata LAFI Dominik Geißler Technische Universität Berlin, Tobias Winkler RWTH Aachen University File Attached

16:00 - 18:00	Fourth SessionLAFI at Salle 13 Chair(s): Guillaume Baudart Inria

16:00 10m Talk		Multi-Agent Systems for Traceable Bayesian Workflow LAFI Xianda Sun University of Cambridge, Andrew D. Gordon Cogna and University of Edinburgh, Hong Ge University of Cambridge File Attached
16:12 10m Talk		Grammar-Constrained LLM Generation for Reliable and Efficient Probabilistic Program Synthesis LAFI Madhav Kanda University of Illinois Urbana-Champaign, Shubham Ugare Meta, Sasa Misailovic University of Illinois at Urbana-Champaign
16:24 10m Talk		Language-Model Probabilistic Programming for Improving Autoformalization via Cycle Consistency and Incremental Type-Checking LAFI Mauricio Barba da Costa MIT, Fabian Zaiser MIT, Katherine Collins MIT, Romir Patel MIT, Timothy O'Donnell , Alexander K. Lew Yale University, Joshua B. Tenenbaum Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology, Cameron Freer Massachusetts Institute of Technology
16:35 80m Poster		Poster Session LAFI

Mon 12 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

11:00 - 12:30	Session 1TPSA at Salle 13

11:00 3m Talk		In Memoriam: Richard Bornat TPSA
11:03 43m Keynote		Building the Cloud with Continuous Assurances using Static Analysis TPSA Subarno Banerjee Amazon Web Services
11:46 22m Talk		Tracking Dynamically Bound Variable Dependencies TPSA Tsung-Han Liu EPFL, Basil L. Contovounesios , Yawen Guan EPFL, Clément Pit-Claudel EPFL
12:08 22m Talk		Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach TPSA Rini Banerjee University of Cambridge, Zain K Aamer University of Pennsylvania, Hiroyuki Katsura University of Cambridge, David Kaloper-Meršinjak University of Cambridge, Dimitrios J. Economou University of Cambridge, Kayvan Memarian University of Cambridge, Dhruv Makwana University of Cambridge, Neel Krishnaswami University of Cambridge, Benjamin C. Pierce University of Pennsylvania, Christopher Pulte University of Cambridge, Peter Sewell University of Cambridge

14:00 - 15:30	Session 2TPSA at Salle 13

14:00 22m Talk		Soteria Rust: Efficient Symbolic Execution for Rust TPSA Opale Sjöstedt Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London
14:22 22m Talk		Towards automatic functional correctness in the Mopsa static analyzer TPSA Milla Valnet Sorbonne Université, Raphaël Monat Inria and University of Lille, Antoine Miné Sorbonne Université
14:45 22m Talk		An LLVM frontend for Infer for Swift analysis TPSA Dulma Churchill Meta
15:07 22m Talk		Specialisation: Context-Dependent Reasoning in Incorrectness Separation Logic TPSA Raquel Fernandes da Silva Imperial College London, Sacha-Élie Ayoun Imperial College London, Azalea Raad Imperial College London, David Pichardie Meta

16:00 - 17:30	Session 3TPSA at Salle 13

16:00 22m Talk		How to identify security vulnerabilities in Node.js packages? TPSA José Fragoso Santos INESC-ID; Instituto Superior Técnico - University of Lisbon, Filipe Marques INESC-ID; Instituto Superior Técnico - University of Lisbon, André Nascimento INESC-ID; Instituto Superior Técnico - University of Lisbon
16:22 22m Talk		Modeling Incorrectness and Unknown Functions with Angelic and Demonic Nondeterminism TPSA Noam Zilberstein Cornell University
16:45 22m Talk		A logic for all reasons TPSA Flavio Ascari University of Konstanz, Roberto Bruni University of Pisa, Lorenzo Gazzella Università di Pisa, Roberta Gori Diaprtimento di Informatica, Universita' di Pisa, Italy
17:07 22m Talk		AMPLE: Fine-grained File Access Policies for Server Applications TPSA Seyedhamed Ghavamnia Bloomberg, Julien Vanegue Imperial College London; Bloomberg

Tue 13 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

09:00 - 10:30	Session 1RTFM at Salle 13

09:00 10m Day opening		Welcome from the Organizers RTFM Amal Ahmed Northeastern University, USA, Derek Dreyer MPI-SWS, Ilya Sergey National University of Singapore
09:10 40m Talk		On long-term research vision RTFM Peter Sewell University of Cambridge
09:50 40m Talk		On transitioning from academia to industry RTFM David Pichardie Meta

11:00 - 12:30	Session 2RTFM at Salle 13

11:00 30m Talk		On building a successful research group RTFM Stephanie Weirich University of Pennsylvania
11:30 60m Panel		Panel: Promotion and tenure RTFM P: Amal Ahmed Northeastern University, USA, P: Lars Birkedal Aarhus University, P: Ilya Sergey National University of Singapore, P: Nicolas Wu Imperial College London, P: Steve Zdancewic University of Pennsylvania, M: Derek Dreyer MPI-SWS

14:00 - 15:30	Session 3RTFM at Salle 13

14:00 40m Talk		On grant writing RTFM Suresh Jagannathan Purdue University
14:40 50m Panel		Panel: Visibility and Impact RTFM P: Derek Dreyer MPI-SWS, P: Xavier Leroy Collège de France - PSL University, P: Nikhil Swamy Microsoft Research, P: Stephanie Weirich University of Pennsylvania, M: Ilya Sergey National University of Singapore

16:00 - 17:30	Session 4RTFM at Salle 13

16:00 60m Panel		Panel: Work-life balance, service, and teaching RTFM P: Sebastian Erdweg KIT, P: Robbert Krebbers Radboud University Nijmegen, P: Azalea Raad Imperial College London, P: Sharon Shoham Tel Aviv University, M: Amal Ahmed Northeastern University, USA

Sat 17 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

09:00 - 10:30	First SessionWITS at Salle 13

09:00 60m Keynote		Lean4Lean: Mechanizing the Metatheory of Lean WITS Mario Carneiro Chalmers University of Technology
10:00 22m Talk		Observing Definitional Equality WITS András Kovács University of Gothenburg and Chalmers University of Technology

11:00 - 12:30	Session 2WITS at Salle 13

11:00 22m Talk		Decoupling Resolution from Type Inference WITS Lionel Parreaux Hong Kong University of Science and Technology
11:22 22m Talk		First-Class Refinement Types in Scala WITS Matt Bovel EPFL
11:45 22m Talk		Types as grammars WITS Gil Silva LASIGE, University of Lisbon, Bernardo Almeida LASIGE, Faculty of Sciences, University of Lisbon, Diana Costa LASIGE, University of Lisbon, Andreia Mordido University of Lisbon, Diogo Poças Instituto de Telecomunicações, University of Lisbon, Vasco T. Vasconcelos LASIGE, University of Lisbon
12:07 22m Talk		Omnidirectional type inference for ML WITS Alistair O'Brien University of Cambridge, Didier Rémy Inria, Gabriel Scherer Université Paris Cité - Inria - CNRS

14:00 - 15:30	Session 3WITS at Salle 13

14:00 22m Talk		A Dependent Language with Type-Safe Program Extraction WITS Greg Brown University of Edinburgh
14:22 22m Talk		Code Generation via Meta-programming in Dependently Typed Proof Assistants WITS Mathis Bouverot-Dupuis INRIA & École Normale Supérieure, Yannick Forster INRIA
14:45 22m Talk		Garbage Collection for Higher Inductive Types WITS Islam Talipov HSE University, Pavel Sokolov HSE University
15:07 22m Talk		Type Inference Techniques: Implementation and Formalization, Better Together WITS Ningning Xie University of Toronto, Andong Fan University of Toronto

16:00 - 18:00	Session 4WITS at Salle 13

16:00 60m Keynote		Verifying Dependent Type-checkers WITS Meven Lennon-Bertrand Inria – Université Paris Cité
17:00 22m Talk		Type Narrowing the Hard Way WITS Ben Greenman University of Utah, Hanwen Guo University of Utah
17:23 2m Other		Closing WITS Niki Vazou IMDEA Software Institute

Sun 11 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
Salle 13	LAFI First Session																								LAFI Second Session																																				LAFI Third Session																								LAFI Fourth Session

Mon 12 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
Salle 13	TPSA																								TPSA Session 1																																				TPSA Session 2																								TPSA Session 3

Tue 13 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
Salle 13	RTFM Session 1																								RTFM Session 2																																				RTFM Session 3																								RTFM Session 4

Sat 17 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
Salle 13	WITS First Session																								WITS Session 2																																				WITS Session 3																								WITS Session 4

Sun 11 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
Salle 13	LAFI Welcome 09:00 - 09:05	LAFI Basis — A Programming Languages Take on Principled Foundations for AI 09:07 - 09:27					LAFI Towards an Equational Calculus of Interventions 09:29 - 09:39		LAFI Typed Abstractions for Causal Probabilistic Programming 09:41 - 09:51			LAFI A Design for Massively Parallel Gibbs Sampling on the GPU via Static an ... 09:53 - 10:03		LAFI A Design Proposal for GraPPL: Probabilistic Programming with Low-Level, ... 10:05 - 10:15											LAFI A Welcome to Causal Probabilistic Programming 11:00 - 11:55											LAFI Verifying Sampling Algorithms via Distributional Invariants 11:56 - 12:06			LAFI Sequential Monte Carlo Program Synthesis with Refinement Proposals 12:08 - 12:18		LAFI A Word Sampler for Well-Typed Functions 12:20 - 12:30																				LAFI Towards Compiling Higher-Order Programs to Bayesian Networks 14:00 - 14:10		LAFI On Contextual Distances in Randomized Programming: Amplification and Lo ... 14:12 - 14:22			LAFI Nominal Semantics for First-class Automatic Differentiation 14:24 - 14:34		LAFI Semantic Foundations for Laziness in Discrete Probabilistic Programming 14:36 - 14:46			LAFI Incremental Density Computation for Efficient Programmable Inference 14:48 - 14:58		LAFI Generating Functions Meet Occupation Measures: Invariant Synthesis for ... 15:00 - 15:10		LAFI Probabilistic Programming Meets Automata Theory: Exact Inference using ... 15:12 - 15:22										LAFI Multi-Agent Systems for Traceable Bayesian Workflow 16:00 - 16:10		LAFI Grammar-Constrained LLM Generation for Reliable and Efficient Probabili ... 16:12 - 16:22			LAFI Language-Model Probabilistic Programming for Improving Autoformalizatio ... 16:24 - 16:34		LAFI Poster Session 16:35 - 17:55

Mon 12 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change


Room	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
Salle 13	TPSA In Memoriam: Richard Bornat 11:00 - 11:03	TPSA Building the Cloud with Continuous Assurances using Static Analysis 11:03 - 11:46								TPSA Tracking Dynamically Bound Variable Dependencies 11:46 - 12:08					TPSA Gradually Retrofitting Assurance into Systems Software: A Separation-Lo ... 12:08 - 12:30																						TPSA Soteria Rust: Efficient Symbolic Execution for Rust 14:00 - 14:22				TPSA Towards automatic functional correctness in the Mopsa static analyzer 14:22 - 14:45					TPSA An LLVM frontend for Infer for Swift analysis 14:45 - 15:07				TPSA Specialisation: Context-Dependent Reasoning in Incorrectness Separation ... 15:07 - 15:30											TPSA How to identify security vulnerabilities in Node.js packages? 16:00 - 16:22				TPSA Modeling Incorrectness and Unknown Functions with Angelic and Demonic N ... 16:22 - 16:45					TPSA A logic for all reasons 16:45 - 17:07				TPSA AMPLE: Fine-grained File Access Policies for Server Applications 17:07 - 17:30

Tue 13 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
Salle 13	RTFM Welcome from the Organizers 09:00 - 09:10		RTFM On long-term research vision 09:10 - 09:50								RTFM On transitioning from academia to industry 09:50 - 10:30														RTFM On building a successful research group 11:00 - 11:30						RTFM Panel: Promotion and tenure 11:30 - 12:30																														RTFM On grant writing 14:00 - 14:40								RTFM Panel: Visibility and Impact 14:40 - 15:30																RTFM Panel: Work-life balance, service, and teaching 16:00 - 17:00

Sat 17 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
Salle 13	WITS Lean4Lean: Mechanizing the Metatheory of Lean 09:00 - 10:00												WITS Observing Definitional Equality 10:00 - 10:22												WITS Decoupling Resolution from Type Inference 11:00 - 11:22				WITS First-Class Refinement Types in Scala 11:22 - 11:45					WITS Types as grammars 11:45 - 12:07				WITS Omnidirectional type inference for ML 12:07 - 12:30																							WITS A Dependent Language with Type-Safe Program Extraction 14:00 - 14:22				WITS Code Generation via Meta-programming in Dependently Typed Proof Assistants 14:22 - 14:45					WITS Garbage Collection for Higher Inductive Types 14:45 - 15:07				WITS Type Inference Techniques: Implementation and Formalization, Better Tog ... 15:07 - 15:30											WITS Verifying Dependent Type-checkers 16:00 - 17:00												WITS Type Narrowing the Hard Way 17:00 - 17:22					WITS Closing 17:23 - 17:25

Room information: Salle 13

Sun 11 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Mon 12 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Tue 13 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Sat 17 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Sun 11 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

LAFI

LAFI

LAFI

LAFI

Mon 12 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

TPSA

TPSA

TPSA

TPSA

Tue 13 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

RTFM

RTFM

RTFM

RTFM

Sat 17 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

WITS

WITS

WITS

WITS

Sun 11 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Mon 12 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Tue 13 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Sat 17 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

Room information: Salle 13

Program Display Configuration

Sun 11 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Mon 12 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Tue 13 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Sat 17 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Sun 11 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

LAFI

LAFI

LAFI

LAFI

Mon 12 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

TPSA

TPSA

TPSA

TPSA

Tue 13 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

RTFM

RTFM

RTFM

RTFM

Sat 17 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

WITS

WITS

WITS

WITS

Sun 11 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Mon 12 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Tue 13 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Sat 17 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change

Sun 11 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Mon 12 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Tue 13 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Sat 17 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Sun 11 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Mon 12 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Tue 13 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Sat 17 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Sun 11 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Mon 12 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Tue 13 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

Sat 17 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change