Program - POPL 2025

Detailed Table Session Timeline Detailed Timeline

Time Zone

The program is currently displayed in (GMT-07:00) Mountain Time (US & Canada).

Use conference time zone: (GMT-07:00) Mountain Time (US & Canada)Select 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 19 Jan
Displayed time zone: Mountain Time (US & Canada) 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
Breakroom																															POPL Catering Break 15:30 - 16:00
Four Square Ballroom																							POPL Catering Lunch 12:30 - 14:00
Hopscotch	Dafny Day opening 09:00 - 09:10		Dafny Keynote 09:10 - 10:10									Dafny Helping users to reduce Brittleness in their Dafny programs - a success ... 11:00 - 11:18		Dafny Towards Proof Stability in SMT-based Program Verification 11:18 - 11:36		Dafny Verifying the Fisher-Yates Shuffle Algorithm in Dafny 11:36 - 11:54			Dafny Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fau ... 11:54 - 12:12		Dafny Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny 12:12 - 12:30								Dafny Baking for Dafny: A CakeML Backend for Dafny 14:00 - 14:18		Dafny Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean 14:18 - 14:36		Dafny Performant, Readable and Interoperable Rust from Dafny 14:36 - 14:54			Dafny Randomised Testing of the Dafny Compiler: Into the CI 14:54 - 15:12		Dafny Teaching Types and Non-Interference in Dafny 15:12 - 15:30				Dafny Laurel: Unblocking Automated Verification with Large Language Models 16:00 - 16:18		Dafny VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Lan ... 16:18 - 16:36		Dafny dafny-annotator: AI-Assisted Verification of Dafny Programs 16:36 - 16:54		Dafny Dafny as Verification-Aware Intermediate Language for Code Generation 16:54 - 17:12		Dafny DafnyBench: A Benchmark for Formal Software Verification 17:12 - 17:30		Dafny Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming 17:30 - 17:48		Dafny Day closing 17:48 - 18:00
Patty Cake	POPL Tutorials Substructural Type Systems 09:00 - 10:30											POPL Tutorials Substructural Type Systems 11:00 - 12:30																	POPL Tutorials MPL: Provably Efficient Parallel Programming 14:00 - 15:30													POPL Tutorials MPL: Provably Efficient Parallel Programming 16:00 - 17:30
Peek-A-Boo	LAFI Welcome 09:00 - 09:05	LAFI Industry Talk: Basis - Programming Languages as Core Technology for AI 09:06 - 09:26			LAFI Towards Symbolic Execution for Probability and Non-determinism 09:27 - 09:42		LAFI Lazy Knowledge Compilation for Discrete PPLs 09:43 - 09:58	LAFI Reasoning About Sampling Without Sampling: Atomic Machines for Contextu ... 09:59 - 10:14	LAFI Exact Inference for Nested Discrete Probabilistic Programs (Remote) 10:15 - 10:30			LAFI Invited talk: TORAX - A Fast and Differentiable Tokamak Transport Simul ... 11:00 - 11:40					LAFI Data-Parallel Differentiation by Optic Composition 11:41 - 11:56		LAFI Data-oriented Design for Differentiable, Probabilistic Programming (Remote) 11:57 - 12:12			LAFI A Domain-Specific PPL for Reasoning about Reasoning (or: a memo on memo) 12:13 - 12:28							LAFI Invited talk: Modern Bayesian Experimental Design 14:00 - 14:40					LAFI Semantics of the memo Probabilistic Programming Language 14:41 - 14:56		LAFI NP-NUTS: A Nonparametric No-U-Turn Sampler 14:57 - 15:12			LAFI Sandwood: Runtime Adaptable Probabilistic Programming for Java (Remote) 15:13 - 15:28			LAFI Partially Evaluating Higher-Order Probabilistic Programs without Stocha ... 16:00 - 16:15	LAFI State Space Model Programming in Turing.jl 16:16 - 16:31		LAFI Poster session 16:32 - 17:27							LAFI Closing remarks 17:28 - 17:30

Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) 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
Breakroom										POPL Catering Break 10:30 - 11:00																												POPL Catering Break 15:30 - 16:00
Dodgeball	WAW Full-Stack Correctness in Wasm: Eliminating Bugs Inside and Outside the ... 09:00 - 09:40				WAW An MLIR Dialect for WebAssembly 09:40 - 10:05			WAW Meta-tracing Interpreters in WebAssembly 10:05 - 10:30				WAW Adventures in Making Wasm Fast and More Secure 11:00 - 11:40				WAW A Coq Formalization of WebAssembly Execution Costs 11:40 - 12:05				WAW The WebAssembly Component Model 12:05 - 12:30								WAW Beyond the Baseline: Experimental WebAssembly for High Performance 14:00 - 14:40				WAWremote Continuing Stack Switching in Wasmtime 14:40 - 15:05				WAW Experience Report: Stack Switching in Wasm SpecTec 15:05 - 15:30				WAWremote A Transactions Extension for Web Assembly 16:00 - 16:25		WAW A Big-Step Compositional Continuation-Passing Semantics for WebAssembly 16:25 - 16:50			WAW Lighting talks and closing discussion 16:50 - 17:30
Duck, Duck Goose	PADL Invited Talk: Solvers, unite! A simple unified semantics for reasoning ... 09:00 - 10:00						PADLBest Student Paper –Honorable Mention Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut Eli ... 10:00 - 10:30					PADL Type-Checking Heterogeneous Sequences in a Simple Embeddable Type System 11:00 - 11:30			PADL Haskell Based Spreadsheets 11:30 - 12:00				PADL The Scenic Route to Deforestation 12:00 - 12:30									PADL A practical approach to handling tabular data in logic 14:00 - 14:30			PADL C3G: Causally Constrained Counterfactual Generation 14:30 - 15:00				PADL On Bridging Prolog and Python to Enhance an Inductive Logic Programming ... 15:00 - 15:30					PADL MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embe ... 16:00 - 16:30			PADL Checking Concurrency Coding Rules 16:30 - 17:00			PADL Can Logic Programming Be Liberated from Predicates and Backtracking? (L ... 17:00 - 17:10	PADL Logic Programming with Extensible Types (Lightning talk) 17:10 - 17:20
Four Square Ballroom																						POPL Catering Lunch 12:30 - 14:00
Hopscotch	VMCAI Keynote Talk: Formal methods in a model-free, data-driven world 09:00 - 10:00						VMCAI Synthesis of Controllers for Continuous Blackbox Systems 10:00 - 10:30					VMCAI Affine Disjunctive Invariant Generation with Farkas’ Lemma 11:00 - 11:30			VMCAI Automatic Inference of Relational Object Invariants 11:30 - 12:00				VMCAI A Static Analysis of Entanglement 12:00 - 12:30									VMCAI Space-Efficient Model-Checking of Higher-Order Recursion Schemes 14:00 - 14:30			VMCAI Parameterized Verification of Systems with Precise (0,1)-Counter Abstra ... 14:30 - 15:00				VMCAI Property-agnostic base case extension for scalable verification of dist ... 15:00 - 15:30					VMCAI ExpectAll: A BDD Based Approach for Link Failure Resilience in Elastic ... 16:00 - 16:30			VMCAI Constructing Trustworthy Smart Contracts 16:30 - 17:00			VMCAIRecorded Automated Flaw Detection for Industrial Robot RESTful Service 17:00 - 17:30
Jax	PriSC Opening Remarks 09:00 - 09:04	PriSC Keynote: Bringing Verified Cryptographic Protocols to Practice 09:05 - 10:04						PriSC A Semantic Approach to Robust Property Preservation 10:05 - 10:30				PriSC ILA: Correctness via Type Checking for Fully Homomorphic Encryption 11:00 - 11:25		PriSC Leveraging Duality for Programming with zkSNARKs 11:25 - 11:49				PriSC Preservation of Speculative Constant-time by Compilation 11:50 - 12:14										PriSC Auditing Rust Crates Effectively 14:00 - 14:24		PriSC Automatic Inference of Enclave Placement in LLVM Compiler 14:25 - 14:49				PriSC Counterexamples in Safe Rust 14:50 - 15:14						PriSC BeePL: Correct-by-compilation kernel extensions 16:00 - 16:24		PriSC Non-Interference Preserving and Optimising Compilation with Hyperproper ... 16:25 - 16:49			PriSC SNIP: Speculative Execution and Non-Interference Preservation for Compi ... 16:50 - 17:14			PriSC Closing Remarks 17:15 - 17:30
Marco Polo	CPP Prospects for Computer Formalization of Infinite-Dimensional Category T ... 09:00 - 10:00						CPPdistinguished paperremote presentation Certifying rings of integers in number fields 10:00 - 10:30					CPPdistinguished paper Split Decisions: Explicit Contexts for Substructural Languages 11:00 - 11:30			CPP Machine Checked Proofs and Programs in Algebraic Combinatorics 11:30 - 12:00				CPPremote presentation Monadic interpreters for concurrent memory models: Executable semantics ... 12:00 - 12:30									CPP An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in T ... 14:00 - 14:30			CPP Intrinsically Correct Sorting in Cubical Agda 14:30 - 15:00				CPP Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear R ... 15:00 - 15:30					CPP Formalized Burrows-Wheeler Transform 16:00 - 16:30			CPPremote presentation Verified and Efficient Matching of Regular Expressions with Lookaround 16:30 - 17:00			CPP Further Tackling Post Correspondence Problem and Proof Generation 17:00 - 17:30
Red Rover	POPL Tutorials Viper: An Infrastructure for Automated Verification in Separation Logic 09:00 - 10:30											POPL Tutorials Viper: An Infrastructure for Automated Verification in Separation Logic 11:00 - 12:30																POPL Tutorials Verification of Distributed Protocols: Decidable Modeling and Invariant ... 14:00 - 15:30												POPL Tutorials Verification of Distributed Protocols: Decidable Modeling and Invariant ... 16:00 - 17:30

Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) 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
Breakroom								POPL Catering Break 10:30 - 11:00																												POPL Catering Break 15:30 - 16:00
Four Square Ballroom																				POPL Catering Lunch 12:30 - 14:00
Hopscotch	VMCAI Keynote Talk: Outcome Logic: a foundational framework for concurrent an ... 09:00 - 10:00					VMCAI 1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes ... 10:00 - 10:30				VMCAI A Real-Blasting Extension of Cvc5 for Reasoning about Floating-Point Ar ... 11:00 - 11:30			VMCAI Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study 11:30 - 12:00				VMCAI Formal Verification of Probabilistic Deep Reinforcement Learning Polici ... 12:00 - 12:30									VMCAI Abstract Local Completeness: A Local form of Abstract Non-Interference 14:00 - 14:30			VMCAI An Abstract Domain for Heap Commutativity 14:30 - 15:00				VMCAI Two-way collaboration between flow and proof in SPARK 15:00 - 15:30					VMCAI LLOR: Automated Repair of OpenMP Programs 16:00 - 16:30			VMCAI Synthesis of Parametric Locally Symmetric Protocols from Abstract Tempo ... 16:30 - 17:00				VMCAI Correctness Witnesses for Concurrent Programs: Bridging the Semantic Di ... 17:00 - 17:30
Keep Away	PADL Invited Talk: Bridging Safety and Performance 09:00 - 10:00					PADLBest student paper SM-based Semantics for Answer Set Programs Containing Conditional Liter ... 10:00 - 10:30				PADL ASP for Language Documentation and Reclamation: A Derivational Stemming ... 11:00 - 11:30			PADL A Weighted Bipolar Argumentation Framework and its ASP-based Implementation 11:30 - 12:00				PADL Automated Playing of Survival Video Games with Commonsense Reasoning (s ... 12:00 - 12:30									PADL Exploring Answer Set Programming for Provenance Graph-Based Cyber Threa ... 14:00 - 14:30			PADLRECORDED Leveraging LLM Reasoning with Dual Horn Programs 14:30 - 15:00				PADLRECORDED Enhancing network diagnosis with reflection in Prolog (extended abstract) 15:00 - 15:30
Marco Polo	CPP CRIS: The power of imagination in specification and verification 09:00 - 10:00					CPPdistinguished paper The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Se ... 10:00 - 10:30				CPP Leakage-Free Probabilistic Jasmin Programs 11:00 - 11:30			CPP Formally verified hardening of C programs against hardware fault injection 11:30 - 12:00				CPPremote presentation CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq 12:00 - 12:30									CPP Nominal Matching Logic With Fixpoints 14:00 - 14:30			CPP Tactic Script Optimisation for Aesop 14:30 - 15:00				CPPremote presentation An Isabelle/HOL Framework for Synthetic Completeness Proofs 15:00 - 15:30					CPP Formalization of Differential Privacy in Isabelle/HOL 16:00 - 16:30			CPP A CHERI C Memory Model for Verified Temporal Safety 16:30 - 17:00				CPP Formalizing the One-way to Hiding Theorem 17:00 - 17:30				CPP Business Meeting 17:30 - 18:00
Paper	POPL Tutorials Stateless Model Checking Concurrent and Distributed Programs 09:00 - 10:30									POPL Tutorials Stateless Model Checking Concurrent and Distributed Programs 11:00 - 12:30
Patty Cake	TPSA Introduction 09:00 - 09:10	TPSAKeynote Improving Static Analysis using Information Collected at Runtime 09:10 - 10:10								TPSA Data Structure Abstraction and Incorrectness Separation Logic 11:00 - 11:18		TPSA Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via G ... 11:18 - 11:36		TPSA Partial Incorrectness Logic 11:36 - 11:54		TPSA Total Outcome Logic: Termination and Nontermination Proving for Effectf ... 11:54 - 12:12		TPSA U-turn: Forward-driven backward analysis for incorrectness 12:12 - 12:30								TPSARemote Compositional Shape Analysis with Shared Abduction and Biabductive Loop ... 14:00 - 14:18		TPSA Calculational design of Incorrectness Separation Logic 14:18 - 14:36		TPSA Scalable Bug Detection for Internally Unsafe Libraries: A Logical Appro ... 14:36 - 14:54		TPSA Enhancing Infer Compositional Analysis with Summary Specialization 14:54 - 15:12		TPSA Cyclic Message Histories for Automated Safety Verification of Distribut ... 15:12 - 15:30				TPSA Distributed transactions over mergeable types: A meta-theory for 5G con ... 16:00 - 16:18		TPSA Domain Reasoning In TopKAT: Reduction and Completeness 16:18 - 16:36		TPSA From Traces to Program Incorrectness: A Type-Theoretic Approach 16:36 - 16:54		TPSA Towards Semantics Lifting for Scientific Computing: A Case Study on FFT 16:54 - 17:12		TPSA Concurrent Quantum Separation Logic for Fine-Grained Parallelism 17:12 - 17:30					POPL Jane Street Game Night 18:00 - 22:00
Peek-A-Boo	PLMW @ POPL Getting the Most Out of POPL 09:00 - 09:45				PLMW @ POPL Icebreaker 09:45 - 10:30					PLMW @ POPL How to give a good talk 11:00 - 11:45					PLMW @ POPL My Journey in Secure Compilation 11:45 - 12:30											PLMW @ POPL From operational semantics to verified compilation (and more) 14:00 - 14:45					PLMW @ POPL A Research Career in Balance 14:45 - 15:30							PLMW @ POPL How to Write Papers So People Can Read Them 16:00 - 16:45					PLMW @ POPL PLMW Panel 16:45 - 17:30
Scissors	PEPM Welcome 09:00 - 09:10	PEPM The Missing Diagonal: High Level Languages for Low Level Systems (Invit ... 09:10 - 10:00				PEPMRemote A Type Safe Calculus for Generating Syntax-Directed Editors 10:00 - 10:30				PEPM The Ethical Compiler: Addressing the Is-Ought Gap in Compilation (Invit ... 11:00 - 11:45					PEPM Algebraic Stepper for Simple Modules 11:45 - 12:15				PEPM Collapsing Towers for Side-Channel Security (Short Paper) 12:15 - 12:30							PEPM A Type-Theoretic Framework for Certified Meta-programming (Invited Talk ... 14:00 - 14:45					PEPM Typed Program Analysis without Encodings 14:45 - 15:15				PEPM A Fuelled Self-Reducer for System T (Short Paper) 15:15 - 15:30			PEPMRemote Type-Sensitive Algebraic Macros (Short Paper) 16:00 - 16:15	PEPM Characterizations of Partial Well-Behaved Lenses 16:15 - 16:45				PEPM Semantics-based program manipulation in the age of LLMs 16:45 - 17:25					PEPM Farewell 17:25 - 17:30
Virtual Only																				POPL Catering SIGPLAN SC Meeting 12:30 - 14:00

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) 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
Breakroom										POPL Catering Break 10:00 - 10:40																							POPL Catering Break 14:20 - 15:00											POPL Catering Break 16:20 - 17:00
Four Square Ballroom																					POPL Catering Lunch 12:00 - 13:20																																POPL Catering POPL Networking Reception 18:00 - 20:00
Four Square Corridor																											POPL Student Research Competition Efficient Strong Simulation of High-level Quantum Gates 18:00 - 20:00 Value semantics in reference-based languages 18:00 - 20:00 Intermittent Concurrency 18:00 - 20:00 APIdemic: Verifying Idempotency of REST API Clients 18:00 - 20:00 Formalizing Erlang’s Success Typings 18:00 - 20:00 A Complete Translation from Planning Problems to linear logic 18:00 - 20:00 Wanco: WebAssembly AOT Compiler that supports Live Migration 18:00 - 20:00 Increasing the Expressiveness of a Gradual Verifier 18:00 - 20:00 M3: A Multi-Stage ML with Mutation 18:00 - 20:00 Loop Invariants Using Neural Networks 18:00 - 20:00 Property Testing Trace Languages 18:00 - 20:00 Optimizing Asynchronous Rust with Hydroflow 18:00 - 20:00 Relational Hoare Logic for Sequential Program Verification 18:00 - 20:00 Expanding the Scope of Grammar-Based Enumerative Testing 18:00 - 20:00 System $F^\omega$ with Coherent Implicit Resolution 18:00 - 20:00 The Store-Order Consistency Testing Problem for C-like Memory Models 18:00 - 20:00 Formalizing Representation Transformations: A Case Study of Bit Vector ... 18:00 - 20:00
Hopscotch																					POPL Catering Mentoring Lunch 12:00 - 13:20
Kick the Can																					POPL Catering PLMW Steering Committee Lunch 12:00 - 13:20
Marco Polo					POPL Welome from the general chair 08:55 - 09:00	POPL Finding Good Programs by Avoiding Bad Ones 09:00 - 10:00							POPL Coinductive Proofs for Temporal Hyperliveness 10:40 - 11:00		POPL Derivative-Guided Symbolic Execution 11:00 - 11:20		POPL Symbolic Automata: omega-Regularity Modulo Theories 11:20 - 11:40		POPL Translation of Temporal Logic for Efficient Infinite-State Reactive Syn ... 11:40 - 12:00								POPL Linear and non-linear relational analyses for Quantum Program Optimization 13:20 - 13:40		POPL Remote Automating equational proofs in Dirac notation 13:40 - 14:00		POPL Flexible Type-Based Resource Estimation in Quantum Circuit Description ... 14:00 - 14:20					POPL A quantitative probabilistic relational Hoare logic 15:00 - 15:20		POPL Approximate Relational Reasoning for Higher-Order Probabilistic Programs 15:20 - 15:40		POPL Compositional imprecise probability: a solution from graded monads and ... 15:40 - 16:00		POPL Sound and Complete Proof Rules for Probabilistic Termination 16:00 - 16:20					POPL Universal Composability is Robust Compilation 17:00 - 17:20		POPL Adversities in Abstract Interpretation - Accommodating Robustness by Ab ... 17:20 - 17:40		POPL Gradual C0: Symbolic Execution for Gradual Verification 17:40 - 18:00
Panzano Restaurant																											POPL Catering Women @ POPL Dinner 19:30 - 22:00
Peek-A-Boo													POPL Maximal Simplification of Polyhedral Reductions 10:40 - 11:00		POPL Program Analysis via Multiple Context Free Language Reachability 11:00 - 11:20		POPL The Best of Abstract Interpretations 11:20 - 11:40		POPL An Incremental Algorithm for Algebraic Program Analysis 11:40 - 12:00								POPL Axe 'Em: Eliminating Spurious States with Induction Axioms 13:20 - 13:40		POPL A Verified Foreign Function Interface Between Coq and C 13:40 - 14:00		POPL Distinguished Paper TensorRight: Automated Verification of Tensor Graph Rewrites 14:00 - 14:20					POPL Consistency of a Dependent Calculus of Indistinguishability 15:00 - 15:20		POPL Finite-Choice Logic Programming 15:20 - 15:40		POPL Denotational Semantics of Gradual Typing using Synthetic Guarded Domain ... 15:40 - 16:00		POPL Abstract Operational Methods for Call-by-Push-Value 16:00 - 16:20					POPL Formal Foundations for Translational Separation Logic Verifiers 17:00 - 17:20		POPL Fulminate: Testing CN Separation-Logic Specifications in C 17:20 - 17:40		POPL Generically Automating Separation Logic by Functors, Homomorphisms, and ... 17:40 - 18:00

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) 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		18:00	15	30	45
Breakroom	POPL Catering Break 10:00 - 10:40																								POPL Catering Break 14:20 - 15:00												POPL Catering Break 16:20 - 17:00
Four Square Ballroom												POPL Catering Lunch 12:00 - 13:20
Hopscotch												POPL Catering Lunch 12:00 - 13:20
Keep Away																		POPL Student Research Competition System $F^\omega$ with Coherent Implicit Resolution 13:20 - 13:33		POPL Student Research Competition Efficient Strong Simulation of High-level Quantum Gates 13:33 - 13:46		POPL Student Research Competition The Store-Order Consistency Testing Problem for C-like Memory Models 13:46 - 14:00	POPL Student Research Competition Wanco: WebAssembly AOT Compiler that supports Live Migration 14:00 - 14:13	POPL Student Research Competition Optimizing Asynchronous Rust with Hydroflow 14:13 - 14:26		POPL Student Research Competition Property Testing Trace Languages 14:26 - 14:40
Kick the Can												POPL Catering SIGPLAN EC meeting 12:00 - 13:20
Marco Polo				POPL Inference Plans for Hybrid Particle Filtering 10:40 - 11:00		POPL Distinguished Paper Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic ... 11:00 - 11:20		POPL Modelling Recursion and Probabilistic Choice in Guarded Type Theory 11:20 - 11:40		POPL Bluebell: An Alliance of Relational Lifting and Independence For Probab ... 11:40 - 12:00								POPL The Decision Problem for Regular First Order Theories 13:20 - 13:40			POPL Distinguished Paper A Primal-Dual Perspective on Program Verification Algorithms 13:40 - 14:00		POPL Dis/Equality Graphs 14:00 - 14:20						POPL A Dependent Type Theory for Meta-programming with Intensional Analysis 15:00 - 15:20		POPL Avoiding signature avoidance in ML modules with zippers 15:20 - 15:40		POPL Bidirectional Higher-Rank Polymorphism with Intersection and Union Types 15:40 - 16:00		POPL Algebraic Temporal Effects: Temporal Verification of Recursively Typed ... 16:00 - 16:20					POPL Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime 17:00 - 17:20		POPL Verifying Quantum Circuits with Level-Synchronized Tree Automata 17:20 - 17:40			POPL SIGPLAN Awards, PC Chair's Report, and Business Meeting 17:50 - 19:00
Patty Cake												POPL Catering LGBTQ+ Lunch 12:00 - 13:20
Peek-A-Boo				POPL RE#: High Performance Derivative-Based Regex Matching with Intersection ... 10:40 - 11:00		POPL Pantograph: A Fluid and Typed Structure Editor 11:00 - 11:20		POPL Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus 11:20 - 11:40		POPL Biparsers: Exact Printing for Data Synchronisation 11:40 - 12:00								POPL Program logics à la carte 13:20 - 13:40			POPL On Extending Incorrectness Logic with Backwards Reasoning 13:40 - 14:00		POPL A Demonic Outcome Logic for Randomized Nondeterminism 14:00 - 14:20						POPL Distinguished Paper Data Race Freedom à la Mode 15:00 - 15:20		POPL RELINCHE: Automatically Checking Linearizability under Relaxed Memory C ... 15:20 - 15:40		POPL Distinguished PaperRemote Relaxed Memory Concurrency Re-executed 15:40 - 16:00		POPL Model Checking C/C++ with Mixed-Size Accesses 16:00 - 16:20					POPL CF-GKAT: Efficient Validation of Control-Flow Transformations 17:00 - 17:20		POPL Algebras for Deterministic Computation are Inherently Incomplete 17:20 - 17:40

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) 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
Breakroom					POPL Catering Break 10:00 - 10:40																							POPL Catering Break 14:20 - 15:00											POPL Catering Break 16:20 - 17:00
Four Square Ballroom																POPL Catering Lunch 12:00 - 13:20
Marco Polo	POPL Welcome to Quantum 3.0! 09:00 - 10:00							POPL MimIR: An Extensible and Type-Safe Intermediate Representation for the ... 10:40 - 11:00		POPL Simple Linear Loops: Algebraic Invariants and Applications 11:00 - 11:20		POPL Automated Program Refinement: Guide and Verify Code Large Language Mode ... 11:20 - 11:40		POPL Remote Tail Modulo Cons, OCaml, and Relational Separation Logic 11:40 - 12:00								POPL Archmage and CompCertCast: End-to-End Verification Supporting Integer-P ... 13:20 - 13:40		POPL Formalising Graph Algorithms with Coinduction 13:40 - 14:00		POPL VeriRT: An End-To-End Verification Framework for Real-Time Distributed ... 14:00 - 14:20					POPL Flo: a Semantic Foundation for Progressive Stream Processing 15:00 - 15:20		POPL Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Se ... 15:20 - 15:40		POPL Semantic Logical Relations for Timed Message-Passing Protocols 15:40 - 16:00		POPL Reachability Analysis of the Domain Name System 16:00 - 16:20					POPL Do You Even Lift? Strengthening Compiler Security Guarantees Against Sp ... 17:00 - 17:20		POPL Preservation of speculative constant-time by compilation 17:20 - 17:40		POPL SNIP: Speculative Execution and Non-Interference Preservation for Compi ... 17:40 - 18:00
Patty Cake																POPL Catering URM Lunch 12:00 - 13:20
Peek-A-Boo								POPL Distinguished Paper Affect: An Affine Type and Effect System 10:40 - 11:00		POPL A modal deconstruction of Löb induction 11:00 - 11:20		POPL QuickSub: Efficient Iso-Recursive Subtyping 11:20 - 11:40		POPL Generic Refinement Types 11:40 - 12:00								POPL BiSikkel: A Multimode Logical Framework in Agda 13:20 - 13:40		POPL Calculational Design of Hyperlogics by Abstract Interpretation 13:40 - 14:00		POPL A Taxonomy of Hoare-Like Logics 14:00 - 14:20					POPL The Duality of λ-Abstraction 15:00 - 15:20		POPL On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus 15:20 - 15:40		POPL Interaction Equivalence 15:40 - 16:00		POPL Distinguished Paper Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for ... 16:00 - 16:20					POPL Progressful Interpreters for Efficient WebAssembly Mechanisation 17:00 - 17:20		POPL Unifying compositional verification and certified compilation with a th ... 17:20 - 17:40		POPL Remote All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants 17:40 - 18:00

Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) 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
Breakroom									POPL Catering Break 10:30 - 11:00																									POPL Catering Break 15:30 - 16:00
Four Square Ballroom																				POPL Catering Lunch 12:30 - 14:00
Keep Away	PLanQCKeynote Unlocking quantum potential with software and compilers 09:00 - 09:45			PLanQCTalk HUGR: A Quantum-Classical Intermediate Representation 09:46 - 10:08			PLanQCTalk QuteFuzz: Fuzzing quantum compilers using randomly generated circuits w ... 10:08 - 10:30				PLanQCTalk The Quantum Abstract Machine 11:00 - 11:22		PLanQCTalk Algebraic and denotational semantics for Classically Controlled Quantum ... 11:22 - 11:45		PLanQCTalk Towards Quantum Multiparty Session Types 11:45 - 12:07		PLanQCTalk Concurrent Quantum Separation Logic for Fine-Grained Parallelism 12:07 - 12:30									PLanQCTalk Verifying the Equivalence of Parameterized Quantum Circuits 14:00 - 14:22		PLanQCTalk An Automata-based Framework for Quantum Circuit Verification 14:22 - 14:45		PLanQC Poster Session 14:45 - 15:30						PLanQCTalkRemote Quantum Register Machine: Efficient Implementation of Quantum Recursive ... 16:00 - 16:22		PLanQCTalk Programming with Projective Cliffords 16:22 - 16:45		PLanQCTalk Proto-Quipper with Reversing and Control 16:45 - 17:07		PLanQCTalk Imperative Quantum Programming with Ownership and Borrowing in Guppy 17:07 - 17:30
Kick the Can	WITS Invited Talk: Type inference in OCaml and GHC using Levels 09:00 - 10:00					WITSRemote Towards Generic Higher-Order Unification Implementations in Haskell 10:00 - 10:30					WITSRemote Towards Generic Type Checking Implementations in Haskell via Second-Ord ... 11:00 - 11:30			WITS McTT: Building A Correct-By-Construction Proof Checker For Martin-Loef ... 11:30 - 12:00		WITSRemote Eta conversion for the unit type (is still not that simple) 12:00 - 12:30										WITS Collaboration Time 1 14:00 - 14:30			WITSRemote Semantic Analysis of Normalisation for Directional Logic Programming 14:30 - 15:00		WITS Incremental Bidirectional Typing via Order Maintenance 15:00 - 15:30					WITS Collaboration Time 2 16:00 - 16:30			WITS Formalizing locally nameless syntax with cofinite quantification 16:30 - 17:00		WITS Closing 17:00 - 17:30
Peek-A-Boo	CoqPL Elpi: rule-based meta-languge for Rocq 09:00 - 09:50				CoqPL Implementing OCaml APIs in Coq 09:50 - 10:10		CoqPL Towards general white-box automation: a typeclass-guided context cleaner 10:10 - 10:30				CoqPL Session with the Coq Development Team 11:00 - 12:10							CoqPL Vellvm: Formalizing the Informal 12:10 - 12:30								CoqPL Towards Verified Linear Algebra Programs Through Equivalence 14:00 - 14:22		CoqPL A Framework of Differential Operators 14:22 - 14:45		CoqPL A Semantic Logical Relation for Termination of Intuitionistic Linear Lo ... 14:45 - 15:07		CoqPL Formal Verification of a Software Defined Delay-Tolerant Network 15:07 - 15:30				CoqPL Towards Automated Verification of LLM-Synthesized C Programs 16:00 - 16:22 CoqNFU: Towards Formalizing NFU in Coq 16:22 - 16:45				CoqPLRemote Participation Towards Mining Robust Coq Proof Patterns 16:45 - 17:07		CoqPLRemote Participation Formal Verification of Quantum Stabilizer Code 17:07 - 17:30

POPL 2025 Program

Sun 19 Jan
Displayed time zone: Mountain Time (US & Canada) change

Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) change

Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) change

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change

Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) change

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

POPL 2025 Program

Switch Program View

Program Display Configuration

Sun 19 JanDisplayed time zone: Mountain Time (US & Canada) change

Mon 20 JanDisplayed time zone: Mountain Time (US & Canada) change

Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change

Wed 22 JanDisplayed time zone: Mountain Time (US & Canada) change

Thu 23 JanDisplayed time zone: Mountain Time (US & Canada) change

Fri 24 JanDisplayed time zone: Mountain Time (US & Canada) change

Sat 25 JanDisplayed time zone: Mountain Time (US & Canada) change

Get Calendar (iCal)

Sun 19 Jan
Displayed time zone: Mountain Time (US & Canada) change

Mon 20 Jan
Displayed time zone: Mountain Time (US & Canada) change

Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) change

Wed 22 Jan
Displayed time zone: Mountain Time (US & Canada) change

Thu 23 Jan
Displayed time zone: Mountain Time (US & Canada) change

Fri 24 Jan
Displayed time zone: Mountain Time (US & Canada) change

Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) change