Program - POPL 2026

Detailed Table Session Timeline Detailed Timeline

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


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		18:00	15	30	45	19:00	15	30	45	20:00	15	30	45	21:00	15	30	45
Halle 1													POPL Catering Break 10:30 - 11:00													POPL Catering Lunch 12:30 - 14:00																			POPL Catering Break 15:30 - 16:00
Horizons	Dafny Day opening 09:00 - 09:12		Dafny Software Verification meets Real-World Cryptography 09:12 - 10:12								Dafny The Design of an Interactive Proof Mode for Dafny 10:12 - 10:30				Dafny Diagnostics in Probabilistic Program Verification 11:00 - 11:18		Dafny Explicit Abstraction Barrier for Autoactive Verification 11:18 - 11:36		Dafny Managing the Proof Context in SPARK 11:36 - 11:54		Dafny Tunable Automation in Automated Program Verification 11:54 - 12:12		Dafny Velvet: A Multi-Modal Verifier for Effectful Programs 12:12 - 12:30									Dafny Lessons from Building an Auto-Active Verifier in Lean 14:00 - 14:18			Dafny Formal Verification of Minimax Algorithms 14:18 - 14:36			Dafny Teaching Automata Theory and Formal Languages with Dafny 14:36 - 14:54			Dafny Verification of E-Voting Algorithms in Dafny 14:54 - 15:12		Dafny A Correct-by-Construction Checker for Validation of Railway Data 15:12 - 15:30				Dafny ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis 16:00 - 16:18			Dafny A benchmark for vericoding: formally verified program synthesis 16:18 - 16:36			Dafny DafnyPro: LLM-Assisted Automated Verification for Dafny Programs 16:36 - 16:54		Dafny MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active ... 16:54 - 17:12		Dafny Specification-Guided Repair of Arithmetic Errors in Dafny Programs usin ... 17:12 - 17:30		Dafny Toward Automated, Contamination-free Dafny Benchmark Generation 17:30 - 17:48			Dafny Day closing 17:48 - 18:00
Salle 12	POPL Tutorials Creusot: Formal verification of Rust programs 09:00 - 10:30														POPL Tutorials Creusot: Formal verification of Rust programs 11:00 - 12:30																	POPL Tutorials Verifying Probabilistic Programs Using Separation Logic 14:00 - 15:30															POPL Tutorials Verifying Probabilistic Programs Using Separation Logic 16:00 - 17:30
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
Salle 14	POPL Tutorials BINSEC: Adapting Symbolic Execution for Binary-level Security 09:00 - 10:30														POPL Tutorials BINSEC: Adapting Symbolic Execution for Binary-level Security 11:00 - 12:30																	POPL Tutorials Discrete and Continuous Models for Concurrent Systems: From Petri Nets ... 14:00 - 15:30															POPL Tutorials Discrete and Continuous Models for Concurrent Systems: From Petri Nets ... 16:00 - 17:30
Salle 19	PriSC Day opening 09:00 - 09:05	PriSC The V8 Sandbox: From Compiler Correctness to Runtime Containment 09:05 - 10:00													PriSC Mind the Boundary: Detecting Undefined Behavior Across Rust’s FFI 11:00 - 11:18		PriSC Specifying ABIs with Realizability and Type-Preserving Compilation 11:18 - 11:36		PriSC Towards formally secure compilation of verified F* programs against unv ... 11:36 - 11:54		PriSC Blame-aware Recomposition for Formally Secure Low-level Compiler Backends 11:54 - 12:12		PriSC WP-Preserving Compilation -- Preserving Weakest Preconditions For End-t ... 12:12 - 12:30									PriSC Efficient Dependency Resolution in IFC-aware Decentralized Programming 14:00 - 14:18			PriSC Tooling Design and Lessons Learned from Systematic Evaluations of the P ... 14:18 - 14:36			PriSC Decompiling for Constant-Time Analysis 14:36 - 14:54			PriSC Modular Verification of Probabilistic Constant-Time 14:54 - 15:12		PriSC GnuZero: A Compiler-Based Zeroization Static Detection Tool for the Masses 15:12 - 15:30				PriSC FSLH: Flexible Mechanized Speculative Load Hardening 16:00 - 16:18			PriSC Towards Robust Secure Compilation in Presence of Speculative Execution 16:18 - 16:36			PriSC Compiling countermeasures against fault attacks with “Tracing LLVM” 16:36 - 16:54		PriSC Modular and automatic formal verification of a RISC-V processor with se ... 16:54 - 17:12		PriSC Fun with flags: How Compilers Break and Fix Constant-Time Code 17:12 - 17:30		PriSC Announcing Security Foundations (new volume of Software Foundations) 17:30 - 17:35	PriSC Day closing 17:35 - 17:40

Mon 12 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
Belvédère	CPP How can Machine Learning Help Formal Proving ? 09:00 - 10:00							CPPdistinguished paper Higher order differential calculus in Mathlib 10:08 - 10:30				CPP Bar Inductive Predicates for Constructive Algebra in Rocq 11:00 - 11:22			CPP Computing Solutions for Systems of Multivariate Ordinary Differential E ... 11:22 - 11:44		CPP Cylindrical Algebraic Decomposition in Coq/Rocq 11:44 - 12:06		CPP Adhesive Category Theory for Graph Rewriting in Rocq 12:06 - 12:28			CPP Formalizing polynomial laws and the universal divided power algebra 12:28 - 12:50							CPP A Certifying Proof Assistant for Synthetic Mathematics in Lean 14:00 - 14:22			CPP Adding Sorts to an Isabelle Formalization of Superposition 14:22 - 14:45		CPP A Lambda-Superposition Tactic for Isabelle/HOL 14:45 - 15:07			CPP Certifying the decidability of the word problem in monoids at large 15:07 - 15:30					CPPdistinguished paper Mechanized Dominator Tree Certification 16:00 - 16:22		CPP Brack: A Verified Compiler for Scheme via CakeML 16:22 - 16:45		CPP Verified VCG and Verified Compiler for Dafny 16:45 - 17:07			CPP Foundational Verification of Running-Time Bounds for Interactive Programs 17:07 - 17:30
Halle 1										POPL Catering Break 10:30 - 11:00												POPL Catering Lunch 12:30 - 14:00																		POPL Catering Break 15:30 - 16:00
Horizons	VMCAI Current State of the Industrial-Strength Infer Static Analysis Platform 09:00 - 10:00						VMCAI Try-Mopsa: Relational Static Analysis in Your Pocket 10:00 - 10:30					VMCAI Data Race Detection by Digest-Driven Abstract Interpretation 11:00 - 11:30				VMCAI Termination Resilience Static Analysis 11:30 - 12:00		VMCAI Forward Symbolic Execution for Trustworthy Automation of Binary Code Ve ... 12:00 - 12:30											VMCAI Understanding Transformers through the Lens of Logic and Automata 14:00 - 15:00							VMCAI Proof Minimization in Neural Network Verification 15:00 - 15:30						VMCAI Verification of Generic VHDL Designs and Their Translation to Rocq 16:00 - 16:30			VMCAIDistinguished Paper A Formal Executable Semantics of PROMELA 16:30 - 17:00			VMCAI Efficient Discovery of Actual Causality in Stochastic Systems 17:00 - 17:30
Salle 12				PADL Declarative Programming: Efficient and reliable programming with human ... 09:30 - 10:30								PADL An efficient compiler for the IDP-Z3 knowledge base system 11:00 - 11:30				PADL Multi-Configurable Search Rules in Prolog and Application to Testing 11:30 - 12:00		PADL Using Prolog to Translate Set Theory and B to SAT 12:00 - 12:30											PADL Property-Based Testing for Asynchronous Functional Reactive Programming ... 14:00 - 14:30				PADL Graph Rewriting Language as a Platform for Quantum Diagrammatic Calculi 14:30 - 15:00			PADL Solving hard combinatorial optimization problems with PyQASP 15:00 - 15:30						PADL Declarative Debugging for Modern Networks 16:00 - 16:30			PADL Interpretable Configuration Optimization for Static Program Verificatio ... 16:30 - 17:00			PADL REGAL: Extracting implicit rules in text using LLMs with logic program ... 17:00 - 17:30
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
Salle 14	PLanQCTalk Opening Address 09:00 - 09:10	PLanQCTalk Traq: Estimating the Quantum Cost of Classical Programs 09:10 - 09:30		PLanQCTalk Programming Abstractions for Quantum Linear Algebra 09:30 - 09:50		PLanQCTalk Verifying Repeat-Until-Success Circuits with AutoQ 09:50 - 10:10		PLanQCTalk VC-Qiskit: Automated–Interactive Verification of Qiskit Passes with Min ... 10:10 - 10:30				PLanQCKeynote Democratizing quantum formal verification: the path-sum way 11:00 - 11:45					PLanQCTalk One rig to control them all 11:45 - 12:05		PLanQCTalk Quantum Coherence Spaces Revisited: A von Neumann (Co)Algebraic Approach 12:05 - 12:25									PLanQCTalk A Graded Modal Type Theory for Pulse Schedules 13:50 - 14:10		PLanQCTalk Efficient Parallel Compilation and Profiling of Quantum Circuits at Lar ... 14:10 - 14:30			PLanQCTalk A Unified Assertion-Based Framework for Classical-Quantum Program Verif ... 14:30 - 14:50		PLanQCRemote A Pulse-Level DSL for Real-Time Quantum Control with Hardware Compilati ... 14:50 - 15:10			PLanQCRemote Quantum Assertion Testing Without Mid-Circuit Measurement: Strategies a ... 15:10 - 15:30				PLanQCPoster Poster Session 16:00 - 16:30			PLanQCTalk Compiling Quantum Lambda-Terms into Circuits via the Geometry of Intera ... 16:30 - 16:50		PLanQCTalk Towards a Hierarchical Quantum Circuit Language 16:50 - 17:10			PLanQCTalk Denotational semantics for stabiliser quantum programs 17:10 - 17:30
Salle 19																													POPL Tutorials A Guided Tour through Oxidized OCaml 14:00 - 15:30													POPL Tutorials A Guided Tour through Oxidized OCaml 16:00 - 17:30
Salle 20	POPL Tutorials Syntactically and Semantically Constraining LLMs with Guarantees using ... 09:00 - 10:30											POPL Tutorials Syntactically and Semantically Constraining LLMs with Guarantees using ... 11:00 - 12:30																	POPL Tutorials Veil: Automated and Interactive Verification of Transition Systems 14:00 - 15:30													POPL Tutorials Veil: Automated and Interactive Verification of Transition Systems 16:00 - 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	17:00		15	30	45	18:00	15	30	45	19:00	15	30	45	20:00	15	30	45	21:00	15	30	45
Belvédère	CPP Specification, Semantics, and Verification of Quantum Programs 09:00 - 10:00										CPP Business Meeting 10:00 - 10:30						CPP Can we formalise type theory intrinsically without any compromise? A ca ... 11:00 - 11:22		CPP Formalization of a Proof Calculus for Incremental Linearization for Sat ... 11:22 - 11:44		CPP Mechanizing Synthetic Tait Computability in Istari 11:44 - 12:06		CPP Building Blocks for Step-Indexed Program Logics 12:06 - 12:28								CPP Certified Symbolic Finite Transducers: Formalization and Applications t ... 14:00 - 14:22		CPP Enhancing Symbolic Execution with Machine-Checked Safety Proofs 14:22 - 14:45			CPP Layers of Confluence for Actors 14:45 - 15:07		CPP Towards composable proofs of cache coherence protocols 15:07 - 15:30				CPP A Recipe for Modular Verification of Generic Tree Traversals 16:00 - 16:22		CPPdistinguished paper Precise Reasoning about Container-Internal Pointers with Logical Pinning 16:22 - 16:44		CPP Modular Specifications and Implementations of Random Samplers in Higher ... 16:44 - 17:06		CPP Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust 17:06 - 17:28		CPP A Rose Tree is Blooming (Proof Pearl) 17:28 - 17:50
Halle 1															POPL Catering Break 10:30 - 11:00										POPL Catering Lunch 12:30 - 14:00															POPL Catering Break 15:30 - 16:00										POPL Jane Street Game Night 17:30 - 21:30
Horizons	VMCAI TypedC: Spatial Memory Safety for Low Level Programs by Abstract Interp ... 09:00 - 10:00										VMCAI Input-based Three-Valued Abstraction Refinement 10:00 - 10:30						VMCAI Multi-variable Quantification of BDDs in External Memory using Nested S ... 11:00 - 11:30			VMCAI Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT S ... 11:30 - 12:00		VMCAI SAT-Based Synthesis of Minimal Deterministic Real-Time Automata via 3DR ... 12:00 - 12:30									VMCAI Atomic Gliders and Cellular Automata as Language Generators 14:00 - 14:30			VMCAI Reachability in multi-agent transfer systems 14:30 - 15:00			VMCAI A Hybrid Meta-Learning Framework for Adaptive Safe Controller Synthesis ... 15:00 - 15:30					VMCAI Efficiently Verifying Quantum Programs with Few T Gates 16:00 - 16:30			VMCAIDistinguished Paper Finding Photonics Circuits via δ-weakening SMT 16:30 - 17:00		VMCAI Probabilistic Verification for Modular Network-on-Chip Systems 17:00 - 17:30
Salle 12						PADL A positive perspective on term representation (Invited Talk) 09:30 - 10:30											PADL A Functional Logic Perspective on Indentation-Sensitive Parsing (Short ... 11:00 - 11:30			PADL A One-Pass CPS Transform with Simulation on the Nose 11:30 - 12:00		PADL Determinacy Checking for Elpi: an Higher-Order Logic Programming Langua ... 12:00 - 12:30
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
Salle 14	POPL Tutorials Analyzing Shell Scripts 09:00 - 10:30																POPL Tutorials Analyzing Shell Scripts 11:00 - 12:30														POPL Tutorials Is Program Synthesis Soluble in Large Language Models? 14:00 - 15:30											POPL Tutorials Is Program Synthesis Soluble in Large Language Models? 16:00 - 17:30
Salle 19	PEPM Welcome 09:00 - 09:05	PEPM Hole Refinements for Polymorphic Type-and-Example Driven Synthesis 09:05 - 09:35					PEPM Inferring Typing Rules for Contextual Sugars 09:35 - 10:05					PEPM S4 modal sequent calculus as intermediate logic and intermediate langua ... 10:05 - 10:20		PEPM Epistemic Logic for Polyglots (Short Paper) 10:20 - 10:35			PEPM Computation-Tree Semantics: An Algorithmic Approach to Structurally Def ... 11:00 - 11:30			PEPM Towards Lightweight and Efficient Choreographic Cloud Services 11:30 - 12:00		PEPM Incrementalizing Haskell implementation of Putback-based Bidirectional ... 12:00 - 12:15		PEPM Partial Evaluation as a primitive in modern network troubleshooting (Ta ... 12:15 - 12:30							PEPMKeynote Revisiting the Evolution of Effects (Invited Talk) 14:00 - 15:30											PEPM Staging Effect Handlers for Modular Search 16:00 - 16:30			PEPM Holey: Staged Execution from Python to SMT (Talk Proposal) 16:30 - 16:45	PEPM Towards Cumulative Abstract Semantics via Handlers (Short Paper) 16:45 - 17:00	PEPM Retargeting an Abstract Interpreter for a New Language by Partial Evalu ... 17:00 - 17:15		PEPM Closing 17:15 - 17:25
Salle 20	PLMW @ POPL Opening 09:00 - 09:10		PLMW @ POPL SIGPLAN CARES Introduction 09:10 - 09:20		PLMW @ POPL The Art of Living Abroad (and Finding a Good Baguette in New York) 09:20 - 09:40			PLMW @ POPL Icebreaker 09:40 - 10:30									PLMW @ POPL PLMW Panel 11:00 - 11:45				PLMW @ POPL Weak Accept, or: How I Learned to Write Papers and Deal with Reviews 11:45 - 12:30										PLMW @ POPL An Invitation to Quantum Programming Languages 14:00 - 14:45					PLMW @ POPL Industry Panel 14:45 - 15:30						PLMW @ POPL How to Write a Paper 16:00 - 16:45				PLMW @ POPL Effects and Call-by-Push-Value 16:45 - 17:30

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


Room	8:00	15	30	45		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	18:00	15	30	45	19:00	15	30	45	20:00	15	30	45	21: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
Halle 0										POPL Catering Break 10:00 - 10:30																												POPL Catering Break 15:40 - 16:10										POPL POPL networking reception 17:30 - 19:30 POPL Student Research Competition AgdaGDL: A Geometric Deep Learning Framework for Property Certification 17:30 - 19:30 A Concise Type System for Borrow Inference 17:30 - 19:30 Language Model for MPI 17:30 - 19:30 An End-to-end Theory for Compositional Symbolic Execution: From Express ... 17:30 - 19:30 RESpecBench: Rigorous Evaluation of Specification Generation with Autom ... 17:30 - 19:30 Asymptotic Analysis as an Abstract Interpretation 17:30 - 19:30 A specification for Agda Core’s unification algorithm for generic patte ... 17:30 - 19:30 Amortized Analysis of Splay Trees via a Lax Homomorphism 17:30 - 19:30 Handling the Selection Monad, Uniformly 17:30 - 19:30 A Well-behaved Differentiable Logic 17:30 - 19:30 Towards Functional Language Runtimes Without Garbage Collection 17:30 - 19:30 The Expressiveness of Programs via Descriptive Complexity 17:30 - 19:30 Ariadne: Automatically Tuning Generator Weights Using Dynamic Sampling 17:30 - 19:30 Specialisation: Context-Dependent Reasoning in Incorrectness Separation ... 17:30 - 19:30 A Verified Distributed Stream Processing Framework 17:30 - 19:30 Partial Evaluation + Global Analyser = Separate Analyser 17:30 - 19:30 Bootstrapping a Verified Compiler for an Imperative Language in Rocq 17:30 - 19:30 Formally Verified Optimisations for the Pancake Compiler 17:30 - 19:30 Expanding Specification Capabilities of a Gradual Verifier with Pure Fu ... 17:30 - 19:30 Towards a Mechanised Theory of Fully Featured Compositional Symbolic Ex ... 17:30 - 19:30 RUXt: Automatic Compositional Type Safety Refutation 17:30 - 19:30 Save Time and Mechanize 17:30 - 19:30 Region Type System with Bidirectional Multiprompt Delimited Control 17:30 - 19:30 Semantic Completeness of Higher-Order Probabilistic Separation Logics 17:30 - 19:30 Decompilation into Interaction Trees 17:30 - 19:30 Interactive symbolic execution of concurrent programs in a theorem prover 17:30 - 19:30 Interrupt-Aware Variable Analysis for SSD Firmware 17:30 - 19:30 A theory of lists with combinators for SMT solvers 17:30 - 19:30
Halle 1																					POPL Catering Lunch 12:15 - 14:00 Mentoring Lunch 12:15 - 14:00
Kraz restaurant																										POPL Women @ POPL Dinner 19:30 - 22:00
Nef					POPL Welcome from the general chair 08:50 - 09:00	POPL Medium-scale automation for proof assistants 09:00 - 10:00						POPL Domain-Theoretic Semantics for Functional Logic Programming 10:30 - 10:55		POPL Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrus ... 10:55 - 11:20			POPL Hyperfunctions: Communicating Continuations 11:20 - 11:45		POPL Lazy Linearity for a Core Functional Language 11:45 - 12:10										POPL Extensible Data Types with Ad-Hoc Polymorphism 14:00 - 14:25		POPL Let Generalization, Polymorphic Recursion, and Variable Minimization in ... 14:25 - 14:50			POPL Local Contextual Type Inference 14:50 - 15:15		POPL Typing Strictness 15:15 - 15:40					POPL Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Speci ... 16:10 - 16:35			POPL Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling 16:35 - 17:00		POPL Oriented Metrics for Bottom-Up Enumerative Synthesis 17:00 - 17:25
Réfectoire						POPL Medium-scale automation for proof assistants 09:00 - 10:00						POPL Remote Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures 10:30 - 10:55		POPL Distinguished Paper 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
Salle 9																					PLMW @ POPL PLMW Steering Committee Meeting 12:15 - 14:00

Thu 15 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	18:00	15	30	45	19:00	15	30	45	20:00	15	30	45	21: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
Halle 0					POPL Catering Break 09:50 - 10:20				POPL Catering Break 10:30 - 11:00																													POPL Catering Break 15:40 - 16:10
Halle 1																				POPL Catering Lunch 12:00 - 14:00
Monsieur Arthur restaurant																														POPL POPL PC and SC dinner 19:30 - 22:00
Nef			POPL Jacobins Convent and its History 09:30 - 09:50					POPL (TOPLAS) Will it Fit? Verifying Heap Space Bounds of Concurrent Progra ... 10:20 - 10:45			POPL Verifying Almost-Sure Termination for Randomized Distributed Algorithms 10:45 - 11:10			POPL Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs us ... 11:10 - 11:35				POPL The Complexity of Testing Message-Passing Concurrency 11:35 - 12:00										POPL A Lazy, Concurrent Convertibility Checker 14:00 - 14:25			POPL Canonicity for Indexed Inductive-Recursive Types 14:25 - 14:50			POPL Coco: Corecursion with Compositional Heterogeneous Productivity 14:50 - 15:15		POPL Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem ... 15:15 - 15:40					POPL A Family of Sims with Diverging Interests 16:10 - 16:35			POPL Endangered by the Language But Saved by the Compiler: Robust Safety via ... 16:35 - 17:00		POPL PC Chair's Report and Business Meeting 17:00 - 18:30
Rennes Tourist Office	POPL Tour of the Historic City Center 09:00 - 10:00
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 Distinguished Paper Security Reasoning via Substructural Dependency Tracking 16:35 - 17:00
Salle 14																						POPL Catering LGBTQ+ Lunch 12:30 - 14:00
Salle 9																				POPL POPL steering committee meeting 12:00 - 14: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
Halle 0					POPL Catering Break 10:00 - 10:30																											POPL Catering Break 15:40 - 16:10
Halle 1																POPL Catering Lunch 12:15 - 14:00
Nef	POPL Hardware-Software Contracts for High Assurance with Applications to Sid ... 09:00 - 10:00						POPL Distinguished Paper All for One and One for All: Program Logics for Exploiting Internal Det ... 10:30 - 10:55		POPL A Verified High-Performance Composable Object Library for Remote Direct ... 10:55 - 11:20			POPL DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs 11:20 - 11:45		POPL TypeDis: A Type System for Disentanglement 11:45 - 12:10									POPL Optimising Density Computations in Probabilistic Programs via Automatic ... 14:00 - 14:25		POPL Distinguished Paper Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Cond ... 14:25 - 14:50			POPL Remote Probabilistic Programming with Vectorized Programmable Inference 14:50 - 15:15		POPL Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of P ... 15:15 - 15:40					POPL Counting and Sampling Traces in Regular Languages 16:10 - 16:35			POPL Parametrised Verification of Intel-x86 Programs 16:35 - 17:00		POPL General Decidability Results for Systems with Continuous Counters 17:00 - 17:25
Réfectoire	POPL Hardware-Software Contracts for High Assurance with Applications to Sid ... 09:00 - 10:00						POPL Di- is for Directed: First-Order Directed Type Theory via Dinaturality 10:30 - 10:55		POPL Distinguished Paper 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 Distinguished Paper Encode the Cake and Eat It Too: Controlling Computation in Type Theory, ... 14:50 - 15:15		POPL Distinguished PaperRemote 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
Salle 14																	POPL Catering URM Lunch 12:30 - 14: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
Halle 1									POPL Catering Break 10:30 - 11:00										POPL Catering Lunch 12:30 - 14:00														POPL Catering Break 15:30 - 16:00
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
Salle 14	RocqPL Future-Proofing Numerical Accuracy with Formal Specifications 09:00 - 09:45					RocqPL Crane Lowers Rocq Safely into C++ 09:45 - 10:00	RocqPL Specifying and Verifying the NOVA Microhypervisor in Concurrent Separat ... 10:00 - 10:15	RocqPL The HOL-Light library of Multivariate real analysis in Rocq 10:15 - 10:30			RocqPL Session with the Rocq Development Team 11:00 - 11:45				RocqPL Rocq CARVe-ing: A Library for Substructural Meta-Theory 11:45 - 12:00	RocqPL Scalable Type Inference for Intrinsically-Typed Binders 12:00 - 12:15		RocqPL Sulfur: Substitution Generation using a Logical Framework 12:15 - 12:30							RocqPL A systematic approach to "Well-founded recursion done right" 14:00 - 14:15	RocqPL Implementing parametricity in Rocq-ELPI 14:15 - 14:30		RocqPL Enhancing universe polymorphism for Rocq: Algebraic universes, consiste ... 14:30 - 14:45	RocqPL Nested Inductive Types for Rocq and Lean 14:45 - 15:00	RocqPL Trocq parametricity translations for inductives 15:00 - 15:15		RocqPL Verifying Synchronous Dataflow Programs with SMTCoq 15:15 - 15:30			RocqPL Abstract VCG: Tie-breaking rules in VCG mechanism design 16:00 - 16:15	RocqPL Formal Assurance for Railway Interlockings: Verifying Z3 SAT Proofs wit ... 16:15 - 16:30	RocqPL Formalizing a First-order Differentiable Logic with MathComp 16:30 - 16:45	RocqPL Recursive Mutexes in Separation Logic 16:45 - 17:00	RocqPL Towards a Mechanization of the ECMAScript (JavaScript) Proposal "Temporal" 17:00 - 17:15	RocqPL Verification of Templated Code in C++ 17:15 - 17:30		RocqPL Lambda JS à la Carte 17:30 - 17:45
Salle 19		GiacoFest Opening 09:10 - 09:20		GiacoFest Keynote Speech 09:20 - 10:30							GiacoFest Short Talks 11:00 - 12:30

POPL 2026 Program

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

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

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

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

POPL 2026 Program

Switch Program View

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

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

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

Get Calendar (iCal)

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

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

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