POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States
Dates

This program is tentative and subject to change.

You're viewing the program in a time zone which is different from your device's time zone change time zone

Wed 22 Jan

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

10:40 - 12:00
Automata and Temporal PropertiesPOPL at Marco Polo
10:40
20m
Talk
Coinductive Proofs for Temporal Hyperliveness
POPL
Arthur Correnson CISPA Helmholtz Center for Information Security, Bernd Finkbeiner CISPA Helmholtz Center for Information Security
11:00
20m
Talk
Derivative-Guided Symbolic Execution
POPL
Yongwei Yuan Purdue University, Zhe Zhou Purdue University, Julia Belyakova Purdue University, Suresh Jagannathan Purdue University
11:20
20m
Talk
Symbolic Automata: omega-Regularity Modulo Theories
POPL
Margus Veanes Microsoft Research, Thomas Ball Microsoft Research, Gabriel Ebner Microsoft Research, Ekaterina Zhuchko Tallinn University of Technology
11:40
20m
Talk
Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis
POPL
Philippe Heim CISPA Helmholtz Center for Information Security, Rayna Dimitrova CISPA Helmholtz Center for Information Security
Pre-print
10:40 - 12:00
Program AnalysisPOPL at Peek-A-Boo
10:40
20m
Talk
Maximal Simplification of Polyhedral Reductions
POPL
Louis Narmour Colorado State University, Tomofumi Yuki , Sanjay Rajopadhye Colorado State University
11:00
20m
Talk
Program Analysis via Multiple Context Free Language Reachability
POPL
Giovanna Kobus Conrado Hong Kong University of Science and Technology, Adam Husted Kjelstrøm Aarhus University, Jaco van de Pol Aarhus University, Andreas Pavlogiannis Aarhus University
11:20
20m
Talk
The Best of Abstract Interpretations
POPL
Roberto Giacobazzi University of Arizona, Francesco Ranzato Dipartimento di Matematica, University of Padova, Italy
11:40
20m
Talk
An Incremental Algorithm for Algebraic Program Analysis
POPL
Chenyu Zhou University of Southern California, Yuzhou Fang University of Southern California, Jingbo Wang Purdue University, Chao Wang University of Southern California
13:20 - 14:20
Quantum Computing 1POPL at Marco Polo
13:20
20m
Talk
Linear and non-linear relational analyses for Quantum Program Optimization
POPL
Matthew Amy Simon Fraser University, Joseph Lunderville Simon Fraser University
13:40
20m
Talk
Automating equational proofs in Dirac notation
POPL
Yingte Xu MPI-SP and Institute of Software, Chinese Academy of Sciences, Gilles Barthe MPI-SP; IMDEA Software Institute, Li Zhou Institute of Software, Chinese Academy of Sciences
14:00
20m
Talk
Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages
POPL
Andrea Colledan University of Bologna & INRIA Sophia Antipolis, Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis
13:20 - 14:20
Verification 1POPL at Peek-A-Boo
13:20
20m
Talk
Axe 'Em: Eliminating Spurious States with Induction Axioms
POPL
Neta Elad Tel Aviv University, Sharon Shoham Tel Aviv University
13:40
20m
Talk
A Verified Foreign Function Interface Between Coq and C
POPL
Joomy Korkut Bloomberg LP, Kathrin Stark Heriot-Watt University, Andrew W. Appel Princeton University
14:00
20m
Talk
TensorRight: Automated Verification of Tensor Graph Rewrites
POPL
Jai Arora University of Illinois at Urbana-Champaign, Sirui Lu University of Washington, Devansh Jain University of Illinois at Urbana-Champaign, Tianfan Xu University of Illinois at Urbana-Champaign, Farzin Houshmand Google, Phitchaya Mangpo Phothilimthana Google, Mohsen Lesani University of California at Santa Cruz, Praveen Narayanan Google, Karthik Srinivasa Murthy Google, Rastislav Bodík Google Research, Brain Team, Amit Sabne Google, Charith Mendis University of Illinois at Urbana-Champaign
15:00 - 16:20
Probabilistic Programming 1POPL at Marco Polo
15:00
20m
Talk
A quantitative probabilistic relational Hoare logic
POPL
Martin Avanzini Inria, Gilles Barthe MPI-SP; IMDEA Software Institute, Benjamin Gregoire INRIA, Davide Davoli Université Côte d’Azur, Inria
15:20
20m
Talk
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
POPL
Philipp G. Haselwarter Aarhus University, Kwing Hei Li Aarhus University, Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University
Pre-print
15:40
20m
Talk
Compositional imprecise probability: a solution from graded monads and Markov categories
POPL
Jack Liell-Cock University of Oxford, Sam Staton University of Oxford
16:00
20m
Talk
Sound and Complete Proof Rules for Probabilistic Termination
POPL
15:00 - 16:20
Semantic modelsPOPL at Peek-A-Boo
15:00
20m
Talk
Consistency of a Dependent Calculus of Indistinguishability
POPL
Yiyun Liu University of Pennsylvania, Jonathan Chan University of Pennsylvania, Stephanie Weirich University of Pennsylvania
15:20
20m
Talk
Finite-Choice Logic Programming
POPL
Chris Martens Northeastern University, Robert Simmons Independent, Michael Arntzenius None
Pre-print
15:40
20m
Talk
Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory
POPL
Eric Giovannini University of Michigan, Tingting Ding University of Michigan, Max S. New University of Michigan
16:00
20m
Talk
Abstract Operational Methods for Call-by-Push-Value
POPL
Sergey Goncharov University of Birmingham, School of Comp. Sci., Stelios Tsampas FAU Erlangen-Nuremberg, INF 8, Henning Urbat FAU Erlangen-Nuremberg, INF 8
17:00 - 18:00
TOPLASPOPL at Marco Polo
17:00 - 18:00
Separation LogicPOPL at Peek-A-Boo
17:00
20m
Talk
Formal Foundations for Translational Separation Logic Verifiers
POPL
Thibault Dardinier ETH Zurich, Michael Sammler Institute of Science and Technology Austria, Gaurav Parthasarathy ETH Zurich, Alexander J. Summers University of British Columbia, Peter Müller ETH Zurich
17:20
20m
Talk
Fulminate: Testing CN Separation-Logic Specifications in C
POPL
Rini Banerjee University of Cambridge, Kayvan Memarian University of Cambridge, Dhruv Makwana University of Cambridge, Christopher Pulte University of Cambridge, Neel Krishnaswami University of Cambridge, Peter Sewell University of Cambridge
17:40
20m
Talk
Generically Automating Separation Logic by Functors, Homomorphisms, and Modules
POPL
Qiyuan Xu Nanyang Technological University, David Sanan Singapore Institute of Technology, Zhe Hou Griffith University, Xiaokun Luan Peking University, Conrad Watt Nanyang Technological University, Yang Liu Nanyang Technological University

Thu 23 Jan

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

10:40 - 12:00
Probabilistic Programming 2POPL at Marco Polo
10:40
20m
Talk
Inference Plans for Hybrid Particle Filtering
POPL
Ellie Y. Cheng MIT, Eric Atkinson , Guillaume Baudart Inria, Louis Mandel IBM Research, USA, Michael Carbin Massachusetts Institute of Technology
11:00
20m
Talk
Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops
POPL
Fabian Zaiser University of Oxford, Andrzej Murawski University of Oxford, C.-H. Luke Ong NTU
Pre-print
11:20
20m
Talk
Modelling Recursion and Probabilistic Choice in Guarded Type Theory
POPL
Philipp Stassen Aarhus University, Rasmus Ejlers Møgelberg IT University of Copenhagen, Maaike Annebet Zwart IT University of Copenhagen, Alejandro Aguirre Aarhus University, Lars Birkedal Aarhus University
11:40
20m
Talk
Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
POPL
Jialu Bao Cornell University, Emanuele D'Osualdo University of Konstanz, Azadeh Farzan University of Toronto
10:40 - 12:00
Syntax and EditingPOPL at Peek-A-Boo
10:40
20m
Talk
RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement and Restricted Lookarounds
POPL
Ian Erik Varatalu Tallinn University of Technology, Estonia, Margus Veanes Microsoft Research, Juhan Ernits Tallinn University of Technology
11:00
20m
Talk
Pantograph: A Fluid and Typed Structure Editor
POPL
Jacob Prinz University of Maryland, College Park, Henry Blanchette , Leonidas Lampropoulos University of Maryland, College Park
11:20
20m
Talk
Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
POPL
Michael D. Adams National University of Singapore, Eric Griffis University of Michigan, Thomas J. Porter University of Michigan, Sundara Vishnu Satish University of Michigan - Ann Arbor, Eric Zhao Brown University, Cyrus Omar University of Michigan
11:40
20m
Talk
Biparsers: Exact Printing for Data Synchronisation
POPL
Ruifeng Xie Peking University, Tom Schrijvers KU Leuven, Zhenjiang Hu Peking University
13:20 - 14:20
Decision ProceduresPOPL at Marco Polo
13:20
20m
Talk
The Decision Problem for Regular First Order Theories
POPL
Umang Mathur National University of Singapore, David Mestel Maastricht University, Mahesh Viswanathan University of Illinois at Urbana-Champaign
13:40
20m
Talk
A Primal-Dual Perspective on Program Verification Algorithms
POPL
Takeshi Tsukada Chiba University, Hiroshi Unno Tohoku University, Oded Padon Weizmann Institute of Science, Sharon Shoham Tel Aviv University
14:00
20m
Talk
Dis/Equality Graphs
POPL
George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Jahrim Gabriele Cesario University of St. Gallen, Guido Salvaneschi University of St. Gallen
13:20 - 14:20
Program Logics 1POPL at Peek-A-Boo
13:20
20m
Talk
Program logics à la carte
POPL
Max Vistrup ETH Zurich, Michael Sammler Institute of Science and Technology Austria, Ralf Jung ETH Zurich
13:40
20m
Talk
On Extending Incorrectness Logic with Backwards Reasoning
POPL
Freek Verbeek Open Universiteit & Virginia Tech, Md Syadus Sefat Virginia Tech, Zhoulai Fu State University of New York, Korea, Binoy Ravindran Virginia Tech
14:00
20m
Talk
A Demonic Outcome Logic for Randomized Nondeterminism
POPL
Noam Zilberstein Cornell University, Dexter Kozen Cornell University, Alexandra Silva Cornell University, Joseph Tassarotti New York University
15:00 - 16:20
ConcurrencyPOPL at Peek-A-Boo
15:00
20m
Talk
Data Race Freedom à la Mode
POPL
Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Benjamin Peters MPI-SWS, Laila Elbeheiry MPI-SWS, Leo White Jane Street, Stephen Dolan Jane Street, Richard A. Eisenberg Jane Street, Chris Casinghino Jane Street, François Pottier Inria, Derek Dreyer MPI-SWS
15:20
20m
Talk
RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
POPL
15:40
20m
Talk
Relaxed Memory Concurrency Re-executed
POPL
Evgenii Moiseenko JetBrains Research, Matteo Meluzzi TU Delft, the Netherlands, Innokentii Meleshchenko JetBrains Research, Neapolis University Pafos, Cyprus, Ivan Kabashnyi JetBrains Research, Constructor University Bremen, Germany, Anton Podkopaev JetBrains Research, Constructor University, Soham Chakraborty TU Delft
16:00
20m
Talk
Model Checking C/C++ with Mixed-Size Accesses
POPL
17:00 - 17:40
Quantum Computing 2POPL at Marco Polo
17:00
20m
Talk
Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
POPL
Kengo Hirata University of Edinburgh, Chris Heunen University of Edinburgh
17:20
20m
Talk
Verifying Quantum Circuits with Level-Synchronized Tree Automata
POPL
Parosh Aziz Abdulla Uppsala University, Sweden, Yo-Ga Chen Academia Sinica, Yu-Fang Chen Academia Sinica, Lukáš Holík Brno University of Technology, Ondřej Lengál Brno University of Technology, Jyun-Ao Lin National Taipei University of Technology, Fang-Yi Lo Academia Sinica, Wei-Lun Tsai Academia Sinica
17:00 - 17:40
Kleene Algebra with TestsPOPL at Peek-A-Boo
17:00
20m
Talk
CF-GKAT: Efficient Validation of Control-Flow Transformations
POPL
Cheng Zhang University College London (UCL), Tobias Kappé LIACS, Leiden University, David E. Narváez Virginia Tech, Nico Naus Open University of The Netherlands & Virginia Tech
17:20
20m
Talk
Algebras for Deterministic Computation are Inherently Incomplete
POPL
Balder ten Cate ILLC, University of Amsterdam, Tobias Kappé LIACS, Leiden University

Fri 24 Jan

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

10:40 - 12:00
Synthesis and CompilationPOPL at Marco Polo
10:40
20m
Talk
MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
POPL
Roland Leißa University of Mannheim, School of Business Informatics and Mathematics, Marcel Ullrich Saarland University, Joachim Meyer Compiler Design Lab; Saarland Informatics Campus; Saarland University, Sebastian Hack Saarland University, Saarland Informatics Campus
11:00
20m
Talk
Simple Linear Loops: Algebraic Invariants and Applications
POPL
Rida Ait El Manssour CNRS & IRIF, Paris, George Kenison Liverpool John Moores University, Mahsa Shirmohammadi CNRS & IRIF, Paris, Anton Varonka TU Wien
11:20
20m
Talk
Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus
POPL
Yufan Cai National University of Singapore, Zhe Hou Griffith University, David Sanan Nanyang Technological University, Singapore, Xiaokun Luan Peking University, Yun Lin Shanghai Jiao Tong University, Jun Sun Singapore Management University, Jin Song Dong National University of Singapore
11:40
20m
Talk
Tail Modulo Cons, OCaml, and Relational Separation Logic
POPL
Clément Allain INRIA, Frédéric Bour Tarides, Basile Clément OCamlPro, François Pottier Inria, Gabriel Scherer Université Paris Cité - Inria - CNRS
10:40 - 12:00
Types 2POPL at Peek-A-Boo
10:40
20m
Paper
Affect: An Affine Type and Effect System
POPL
Orpheas van Rooij University of Edinburgh, Robbert Krebbers Radboud University Nijmegen
Link to publication
11:00
20m
Talk
A modal deconstruction of Löb induction
POPL
Daniel Gratzer Aarhus University
11:20
20m
Talk
QuickSub: Efficient Iso-Recursive Subtyping
POPL
Litao Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
11:40
20m
Talk
Generic Refinement Types
POPL
13:20 - 14:20
Verification 2POPL at Marco Polo
13:20
20m
Talk
Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
POPL
Yonghyun Kim Seoul National University, South Korea, Minki Cho Seoul National University, Jaehyung Lee Seoul National University, Jinwoo Kim Seoul National University, Taeyoung Yoon Seoul National University, Youngju Song MPI-SWS, Chung-Kil Hur Seoul National University
13:40
20m
Research paper
Formalising Graph Algorithms with Coinduction
POPL
Donnacha Oisín Kidney Imperial College London, Nicolas Wu Imperial College London
Pre-print
14:00
20m
Talk
VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems
POPL
Yoonseung Kim Yale University, Sung-Hwan Lee Seoul National University, Yonghyun Kim Seoul National University, South Korea, Chung-Kil Hur Seoul National University
13:20 - 14:20
Program Logics 2POPL at Peek-A-Boo
13:20
20m
Talk
BiSikkel: A Multimode Logical Framework in Agda
POPL
Joris Ceulemans KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese KU Leuven
13:40
20m
Talk
Calculational Design of Hyperlogics by Abstract Interpretation
POPL
Patrick Cousot , Jeffery Wang CIMS, New York University
14:00
20m
Talk
A Taxonomy of Hoare-Like Logics
POPL
Lena Verscht RWTH Aachen University; Saarland University, Benjamin Lucien Kaminski Saarland University; University College London
15:00 - 16:20
Concurrency 2POPL at Marco Polo
15:00
20m
Talk
Flo: a Semantic Foundation for Progressive Stream Processing
POPL
Shadaj Laddad University of California at Berkeley, Alvin Cheung University of California at Berkeley, Joseph M. Hellerstein UC Berkeley, Mae Milano Princeton University
Pre-print
15:20
20m
Talk
Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types
POPL
Thien Udomsrirungruang University of Oxford, Nobuko Yoshida University of Oxford
15:40
20m
Talk
Semantic Logical Relations for Timed Message-Passing Protocols
POPL
Yue Yao Carnegie Mellon University, Grant Iraci University at Buffalo, Cheng-En Chuang University at Buffalo, Stephanie Balzer Carnegie Mellon University, Lukasz Ziarek University at Buffalo
16:00
20m
Talk
Reachability Analysis of the Domain Name System
POPL
Dhruv Nevatia ETH Zurich, Si Liu ETH Zurich, David Basin ETH Zurich
15:00 - 16:20
TheoryPOPL at Peek-A-Boo
15:00
20m
Talk
The Duality of λ-Abstraction
POPL
Vikraman Choudhury Università di Bologna & Inria OLAS, Simon J. Gay University of Glasgow, UK
15:20
20m
Talk
On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
POPL
Naoki Kobayashi University of Tokyo
15:40
20m
Talk
Interaction Equivalence
POPL
Beniamino Accattoli Inria & Ecole Polytechnique, Adrienne Lancelot Inria, LIX Ecole Polytechnique, IRIF Université Paris Cité, Giulio Manzonetto Université Paris Cité, Gabriele Vanoni IRIF, Université Paris Cité
16:00
20m
Talk
Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings
POPL
Jan van Brügge Heriot-Watt University, James McKinna Heriot-Watt University, Andrei Popescu University of Sheffield, Dmitriy Traytel University of Copenhagen
17:00 - 18:00
Speculative ExecutionPOPL at Marco Polo
17:00
20m
Talk
Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
POPL
Xaver Fabian CISPA, Marco Patrignani University of Trento, Marco Guarnieri IMDEA Software Institute, Michael Backes Cispa Helmholtz Center for Information Security
17:20
20m
Talk
Preservation of speculative constant-time by compilation
POPL
Santiago Arranz Olmos Max Planck Institute for Security and Privacy, Gilles Barthe MPI-SP; IMDEA Software Institute, Lionel Blatter Max Planck Institute for Security and Privacy, Benjamin Gregoire INRIA, Vincent Laporte Inria
17:40
20m
Talk
SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
POPL
Sören van der Wall PhD Student, Roland Meyer TU Braunschweig
17:00 - 18:00
Proof AssistantsPOPL at Peek-A-Boo
17:00
20m
Talk
Progressful Interpreters for Efficient WebAssembly Mechanisation
POPL
Xiaojia Rao Imperial College London, Stefan Radziuk Imperial College London, Conrad Watt Nanyang Technological University, Philippa Gardner Imperial College London
17:20
20m
Talk
Unifying compositional verification and certified compilation with a three-dimensional refinement algebra
POPL
Yu Zhang , Jérémie Koenig Yale University, Zhong Shao Yale University, Yuting Wang Shanghai Jiao Tong University
17:40
20m
Talk
All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
POPL
Josselin Poiret Nantes Université, Inria, Gaetan Gilbert , Kenji Maillard Inria, Pierre-Marie Pédrot INRIA, Matthieu Sozeau Inria, Nicolas Tabareau Inria, Éric Tanter University of Chile

Accepted Papers

Title
Abstract Operational Methods for Call-by-Push-Value
POPL
A Demonic Outcome Logic for Randomized Nondeterminism
POPL
A Dependent Type Theory for Meta-programming with Intensional Analysis
POPL
Affect: An Affine Type and Effect System
POPL
Link to publication
Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs
POPL
Algebras for Deterministic Computation are Inherently Incomplete
POPL
All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
POPL
A modal deconstruction of Löb induction
POPL
An Incremental Algorithm for Algebraic Program Analysis
POPL
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
POPL
Pre-print
A Primal-Dual Perspective on Program Verification Algorithms
POPL
A quantitative probabilistic relational Hoare logic
POPL
Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting
POPL
A Taxonomy of Hoare-Like Logics
POPL
Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus
POPL
Automating equational proofs in Dirac notation
POPL
A Verified Foreign Function Interface Between Coq and C
POPL
Avoiding signature avoidance in ML modules with zippers
POPL
Axe 'Em: Eliminating Spurious States with Induction Axioms
POPL
Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings
POPL
Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
POPL
Biparsers: Exact Printing for Data Synchronisation
POPL
BiSikkel: A Multimode Logical Framework in Agda
POPL
Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
POPL
Calculational Design of Hyperlogics by Abstract Interpretation
POPL
CF-GKAT: Efficient Validation of Control-Flow Transformations
POPL
Coinductive Proofs for Temporal Hyperliveness
POPL
Compositional imprecise probability: a solution from graded monads and Markov categories
POPL
Consistency of a Dependent Calculus of Indistinguishability
POPL
Data Race Freedom à la Mode
POPL
Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory
POPL
Derivative-Guided Symbolic Execution
POPL
Dis/Equality Graphs
POPL
Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
POPL
Finite-Choice Logic Programming
POPL
Pre-print
Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages
POPL
Flo: a Semantic Foundation for Progressive Stream Processing
POPL
Pre-print
Formal Foundations for Translational Separation Logic Verifiers
POPL
Formalising Graph Algorithms with Coinduction
POPL
Pre-print
Fulminate: Testing CN Separation-Logic Specifications in C
POPL
Generically Automating Separation Logic by Functors, Homomorphisms, and Modules
POPL
Generic Refinement Types
POPL
Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
POPL
Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops
POPL
Pre-print
Inference Plans for Hybrid Particle Filtering
POPL
Interaction Equivalence
POPL
Linear and non-linear relational analyses for Quantum Program Optimization
POPL
Maximal Simplification of Polyhedral Reductions
POPL
MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
POPL
Model Checking C/C++ with Mixed-Size Accesses
POPL
Modelling Recursion and Probabilistic Choice in Guarded Type Theory
POPL
On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
POPL
On Extending Incorrectness Logic with Backwards Reasoning
POPL
Pantograph: A Fluid and Typed Structure Editor
POPL
Preservation of speculative constant-time by compilation
POPL
Program Analysis via Multiple Context Free Language Reachability
POPL
Program logics à la carte
POPL
Progressful Interpreters for Efficient WebAssembly Mechanisation
POPL
QuickSub: Efficient Iso-Recursive Subtyping
POPL
Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
POPL
Reachability Analysis of the Domain Name System
POPL
RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement and Restricted Lookarounds
POPL
Relaxed Memory Concurrency Re-executed
POPL
RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
POPL
Semantic Logical Relations for Timed Message-Passing Protocols
POPL
Simple Linear Loops: Algebraic Invariants and Applications
POPL
SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
POPL
Sound and Complete Proof Rules for Probabilistic Termination
POPL
Symbolic Automata: omega-Regularity Modulo Theories
POPL
Tail Modulo Cons, OCaml, and Relational Separation Logic
POPL
TensorRight: Automated Verification of Tensor Graph Rewrites
POPL
The Best of Abstract Interpretations
POPL
The Decision Problem for Regular First Order Theories
POPL
The Duality of λ-Abstraction
POPL
Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types
POPL
Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis
POPL
Pre-print
Unifying compositional verification and certified compilation with a three-dimensional refinement algebra
POPL
Verifying Quantum Circuits with Level-Synchronized Tree Automata
POPL
VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems
POPL

POPL 2025 Call for Papers

PACMPL Issue POPL 2025 seeks contributions on all aspects of programming languages and programming systems, both theoretical and practical. Authors of papers published in PACMPL Issue POPL 2025 will be invited to present their work in the POPL conference in January 2025, which is sponsored by ACM SIGPLAN, in cooperation with ACM SIGACT and ACM SIGLOG.

Scope

Principles of Programming Languages (POPL) is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome, on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation, or application of programming languages.

Evaluation Criteria

The Review Committee will evaluate the technical contribution of each submission as well as its accessibility to both experts and the general POPL audience. All papers will be judged on significance, originality, relevance, correctness, and clarity. Each paper must explain its scientific contribution in both general and technical terms, identifying what has been accomplished, explaining why it is significant, and comparing it with previous work. Advice on writing technical papers can be found on the SIGPLAN author information page.

Deadlines and formatting requirements, detailed below, will be strictly enforced.

Double-Blind Reviewing

POPL 2025 will use a full double-blind reviewing process (similar to the one used for POPL 2023 and 2024 but different from the lightweight double-blind process used in previous years). This means that identities of authors will not be made visible to reviewers until after conditional-acceptance decisions have been made, and then only for the conditionally-accepted papers. The use of full double-blind reviewing has several consequences for authors.

  • Submissions: Authors must omit their names and institutions from their paper submissions. In addition, references to authors’ own prior work should be in the third person (e.g., not “We build on our previous work …” but rather “We build on the work of …”).

  • Supplementary material: Authors are permitted to provide supplementary material (e.g., detailed proofs, proof scripts, system implementations, or experimental data) along with their submission, which reviewers may (but are not required to) examine. This material may take the form of a single file, such as a PDF or a tarball. Authors must fully anonymize any supplementary material.

  • Author response: In responding to reviews, authors should not say anything that reveals their identity, since author identities will not be revealed to reviewers at that stage of the reviewing process.

  • Dissemination of work under submission: Authors are welcome to disseminate their ideas and post draft versions of their paper(s) on their personal website, institutional repository, or arXiv (reviewers will be asked to turn off arXiv notifications during the review period). But authors should not take steps that would almost certainly reveal their identities to members of the Program Committee, e.g., directly contacting PC members or publicizing the work on widely-visible social media or major mailing lists used by the community.

The purpose of the above restrictions is to help the Program Committee and external reviewers come to a judgment about the paper without bias, not to make it impossible for them to discover the authors’ identities if they were to try. In particular, nothing should be done in the name of anonymity that weakens the quality of the submission.

However, there are occasionally cases where adhering to the above restrictions is truly difficult or impossible for one reason or another. In such cases, the authors should contact the Program Chair to discuss the situation and how to handle it.

The FAQ on Double-Blind Reviewing addresses many common scenarios and answers many common questions about this topic. But there remain many grey areas and trade-offs. If you have any doubts about how to interpret the double-blind rules or you encounter a complex case that is not clearly covered by the FAQ, please contact the Program Chair for guidance.

Evaluation Process

Like last year, POPL 2025 will use a double-blind reviewing process (instead of the lightweight double-blind process used in recent years). This means that identities of authors will not be visible to reviewers until after conditional-acceptance decisions have been made. For authors, the main change is that there is no option to upload non-anonymized supplementary material; only anonymized supplementary material may be submitted.

POPL 2025 will have five Associate Chairs who will help the PC Chair monitor reviews, solicit external expert reviews for submissions when there is not enough expertise on the committee, and facilitate reviewer discussions.

As in previous years, authors will have a multi-day period to respond to reviews, as indicated in the Important Dates table. Responses are optional. A response must be concise, addressing specific points raised in the reviews; in particular, it must not introduce new technical results. Reviewers will write a short reaction to these author responses.

The Review Committee (RC) will discuss papers electronically, and will use synchronous virtual meetings to discuss any papers for which there is disagreement among reviewers, in some cases soliciting additional input from other experts in the committee. There is no formal External Review Committee, though experts outside the committee may be consulted for some papers. Reviews will be accompanied by a short summary of the reasons behind the committee’s decision with the goal of clarifying the reasons behind the decision.

To conform with ACM requirements for journal publication, all POPL papers will be conditionally accepted; authors will be required to submit a short description of the changes made to the final version of the paper, including how the changes address any requirements imposed by the Review Committee. That the changes are sufficient will be confirmed by the original reviewers prior to acceptance to POPL. Authors of conditionally accepted papers must submit a satisfactory revision to the Review Committee by the requested deadline or risk rejection.

For additional information about the reviewing process, see: Principles of POPL, a presentation of the underlying organizational and reviewing policies for POPL. For POPL 2025, policies specified in this Call for Papers supersede those in the Principles of POPL document.

Submission Site Information

The submission site is https://popl25.hotcrp.com.

Authors can submit multiple times prior to the deadline. Only the last submission will be reviewed. There is no abstract deadline. The submission site requires entering author names and affiliations, relevant topics, and potential conflicts. Addition or removal of authors after the submission deadline will need to be approved by the Program Chair (as this kind of change potentially undermines the goal of eliminating conflicts during paper assignment).

The submission deadline is 11:59PM July 11, 2024 anywhere on earth: https://en.wikipedia.org/wiki/Anywhere_on_Earth

Conflicts of Interest

For each submission, the authors must make sure that they properly declare all potential conflicts of interest for all of the authors of that submission. This includes marking PC conflicts as well as “Other Conflicts (external)”. A conflict caught late in the reviewing process leads to a voided review which may be infeasible to replace.

Conflicts should be declared between an adviser and an advisee (e.g., Ph.D., post-doc; forever), between an author and a co-author (papers and proposals; for two years), between people at the same institution (branches of large companies or different locations of research institutes are considered to be the same institution; for two years after leaving an institution), between people with financial conflicts of interest, and between friends or relatives.

Please do not declare spurious conflicts: such incorrect conflicts are especially harmful if the aim is to exclude potential reviewers, so spurious conflicts can be grounds for rejection. If you are unsure about a conflict, please consult the Program Chair.

Submission Guidelines

Prior to the paper submission deadline, authors should upload their full anonymized paper. Here are some key requirements concerning paper submissions:

  • Each paper should have no more than 25 pages of text, excluding bibliography, using the PACMPL format (specifically, the acmart LaTeX class with acmsmall option). It is a single-column page layout with a 10 pt font, 12 pt line spacing, and wider margins than recent POPL page layouts. In this format, the main text block is 5.478 in (13.91 cm) wide and 7.884 in (20.03 cm) tall. Use of a different format (e.g., smaller fonts or a larger text block) is grounds for summary rejection. The PACMPL template for LaTeX can be found at the SIGPLAN author information page, and further information about PACMPL submissions can be found on the PACMPL author guidelines page. PACMPL does not support submissions in Microsoft Word.

  • We strongly encourage use of the review and screen options in order to make submissions easier to review.

  • (NEW this year) Authors may choose which citation format they wish to use, which can be either author-year (the mandate for final versions in previous years) or numeric.

  • Submissions should be in PDF and printable on both US Letter and A4 paper. Papers may be resubmitted to the submission site multiple times up until the deadline, but the last version submitted before the deadline will be the version reviewed.

  • Submitted papers must adhere to the SIGPLAN Republication Policy and the ACM Policy on Plagiarism. Concurrent paper submissions to other conferences, workshops, journals, or similar forums of publication are not allowed.

  • Authors are free to submit supplementary material along with their submissions, but it must be fully anonymized.

  • Authors must list all their conflicts of interest (both PC conflicts and external conflicts) in the HotCRP submission form.

  • Authors may include additional information in a field of the HotCRP submission form labeled “Confidential Comments for the Program Chair”. This information need not be anonymized. It can be used to inform the Program Chair, for example, about sensitive issues concerning a conflict with a PC member or about supplementary material that cannot be anonymized. It is left to the discretion of the Program Chair what to do with this information.

  • If for some reason an author feels uncomfortable discussing a sensitive issue with the Program Chair (or communicating via the “Confidential Comments” field in HotCRP), they should feel free to get in touch instead with any of the Associate Chairs, with whom they can discuss the issue in confidence.

  • Submissions from PC members (except the Program Chair) are permitted and will not be handled any differently than other submissions. This is in accordance with a recent change in policy approved by the SIGPLAN Executive Committee: SIGPLAN conferences that use full double-blind review and whose PCs have at least 50 members need not hold PC submissions to a higher standard.

Artifact Evaluation for Accepted Papers

Authors of conditionally accepted papers will be invited to formally submit supporting materials to the Artifact Evaluation process. Artifact Evaluation is run by a separate committee whose task is to assess how the artifacts support the work described in the papers. Artifact submission is strongly encouraged but voluntary and will not influence the final decision regarding the papers. Papers that go through the Artifact Evaluation process successfully will receive a seal of approval printed on the papers themselves. Authors of accepted papers are encouraged to make these materials publicly available upon publication of the proceedings, by including them as “source materials” in the ACM Digital Library.

Copyright, Publication, and Presentation

As a Gold Open Access journal, PACMPL is committed to making peer-reviewed scientific research free of restrictions on both access and (re-)use. Authors are strongly encouraged to support libre open access by licensing their work with the Creative Commons Attribution 4.0 International (CC BY) license, which grants readers liberal (re-)use rights.

Authors of accepted papers will be required to choose one of the following publication rights:

  • Author licenses the work with a Creative Commons license, retains copyright, and (implicitly) grants ACM non-exclusive permission to publish (suggested choice).
  • Author retains copyright of the work and grants ACM a non-exclusive permission to publish license.
  • Author retains copyright of the work and grants ACM an exclusive permission to publish license.
  • Author transfers copyright of the work to ACM.

These choices follow from ACM Copyright Policy and ACM Author Rights, corresponding to ACM’s “author pays” option. While PACMPL may ask authors who have funding for open-access fees to voluntarily cover the article processing charge (currently, US$400), payment is not required for publication. PACMPL and SIGPLAN continue to explore the best models for funding open access, focusing on approaches that are sustainable in the long-term while reducing short-term risk.

All papers will be archived by the ACM Digital Library. Authors will have the option of including supplementary material with their paper. The official publication date is the date the proceedings are made available in the ACM Digital Library. This date may be up to two weeks prior to the first day of the conference. The official publication date affects the deadline for any patent filings related to published work.

Authors of accepted papers are encouraged (but not required) to give a short talk (roughly 25 minutes long) at the conference, according to the conference schedule.

AUTHORS TAKE NOTE:

The official publication date is the date the proceedings are made available in the ACM Digital Library. This date may be up to two weeks prior to the first day of your conference. The official publication date affects the deadline for any patent filings related to published work.

Distinguished Paper Awards

At most 10% of the accepted papers of POPL 2025 will be designated as Distinguished Papers. This award highlights papers that the Review Committee thinks should be read by a broad audience due to their relevance, originality, significance, and clarity. The selection of the distinguished papers will be made based on the final version of the paper and through an additional review process.

General

Q: Why are you using double-blind reviewing?

A: Studies have shown that a reviewer’s attitude toward a submission may be affected, even unconsciously, by the identity of the authors. We want reviewers to be able to approach each submission without any such, possibly involuntary, pre-judgment. Many computer science conferences have embraced double-blind reviewing. POPL has used double-blind reviewing for several years now as stipulated in the Principles of POPL.

Q: Why are you using full double-blind reviewing instead of lightweight double-blind reviewing?

A: For about a decade, POPL used lightweight double-blind review (double-blind until PC members submit reviews). For POPL 2023, the conference switched to full double-blind review (double-blind until conditional acceptance). There are benefits and drawbacks to both approaches, but based on our experience so far, the benefits of full-double blind seem to outweight the drawbacks.

Q: Do you really think blinding actually works? I suspect reviewers can often guess who the authors are anyway.

A: It is relatively rare for authorship to be guessed correctly, even by expert reviewers, as detailed in this study.

Q: Couldn’t blind submission create an injustice where a paper is inappropriately rejected based upon supposedly-prior work which was actually by the same authors and not previously published?

A: Yes, but we have mechanisms in place to prevent such an injustice from occurring. Reviewers are held accountable for their positions and are required to identify any supposed prior work that they believe undermines the novelty of the paper. Any assertion that “this has been done before” by reviewers should be supported with concrete information. The author response mechanism exists in part to hold reviewers accountable for claims that may be incorrect. Moreover, if authors believe that their paper is being misjudged due to the constraints of double-blind review, they should feel free to get in touch with the Program Chair.

For authors

Q: What exactly do I have to do to anonymize my paper?

A: Use common sense. Your job is not to make your identity undiscoverable but simply to make it possible for reviewers to evaluate your submission without having to know who you are. The specific guidelines stated in the call for papers are simple: omit authors’ names from your title page, and when you cite your own work, refer to it in the third person. For example, if your name is Smith and you have worked on amphibious type systems, instead of saying “We extend our earlier work on statically typed toads [Smith 2004],” you might say “We extend Smith’s [2004] earlier work on statically typed toads.” Also, be sure not to include any acknowledgements that would give away your identity, and avoid revealing the institutional affiliation of authors or at which the work was performed.

If you believe for some reason that it is impossible to anonymize your paper without significantly weakening it, please feel free to get in touch with the Program Chair to discuss the situation.

Q: I would like to provide supplementary material for consideration, e.g., the code of my implementation or proofs of theorems. How do I do this?

A (and also see the next question): On the submission site there will be an option to submit supplementary material along with your main paper. This supplementary material should also be anonymized; it may be viewed by reviewers during the review period, so it should adhere to the same double-blind guidelines.

Q: My submission is based on code available in a public repository or I would like to provide a link to an online demo. How do I deal with this?

A: We discourage the use of external links, but sometimes the most convenient way to share suplementary material such as code or datasets is to include a link to a github repository or a google drive, but it is very important that they are fully anonymized. In particular, a link to your working code repository that exposes the identities of the contributors will be in violation of the double blind policy.

The same holds for online demos; reviewers should be able to visit the online demo and potentially browse its source code without being exposed to the identity of the authors (watch out for copyright statements, for example).

You should keep in mind that reviewers are under no obligation to review any supplementary material, including externally linked data or code, and reviewers may chose not to visit any externally linked material.

Needless to say, attempting to discover the reviewers for your paper by tracking visitors to a public repository or an online demo would constitute a breach of academic integrity.

Q: I am building on my own past work on the WizWoz system. Do I need to rename this system in my paper for purposes of anonymity, so as to remove the implied connection between my authorship of past work on this system and my present submission?

A: No. The relationship between systems and authors changes over time, so there will be at least some doubt about authorship. Increasing this doubt by changing the system name would help with anonymity, but it would compromise the research process. In particular, changing the name requires explaining a lot about the system again because you can’t just refer to the existing papers, which use the proper name. Not citing these papers runs the risk of the reviewers who know about the existing system thinking you are replicating earlier work. It is also confusing for the reviewers to read about the paper under Name X and then have the name be changed to Name Y. Will all the reviewers go and re-read the final version with the correct name? If not, they have the wrong name in their heads, which could be harmful in the long run.

Q: I am submitting a paper that extends my own work that previously appeared at a workshop. Should I anonymize any reference to that prior work?

A: If the previous workshop publication resulted in a published paper, then your POPL submission will be judged on the significance of its delta with respect to that earlier paper. In that case, you should definitely cite the earlier paper as you would any other paper (i.e., in the third person, not revealing that you were the author of the earlier paper) and explain the delta. If, on the other hand, the work presented at an earlier workshop was not accompanied by a proper publication (e.g., if it was just a talk), then your POPL submission may very well have significant overlap with it and citing the workshop work would effectively unblind your paper. In such a case, it is not necessary to cite the earlier presentation. Instead, please mention it in the “Confidential Comments for the Program Chair” field of the HotCRP form so that the Program Chair is aware of the situation. When in doubt, ask the Program Chair for guidance.

Q: I want to cite some related work that itself cites an earlier version of my paper/system that appeared previously online. But that would effectively unblind my submission. What do I do?

A: It is difficult to give a general answer to this question. Ask the Program Chair for guidance.

Q: My submission presents a technique that I employed in the development of previous papers but which was never properly described in those papers. If I mention that my technique was used in those previous papers, I am effectively unblinding my submission, but if I don’t mention it, reviewers may think I am ripping off my own prior work. What do I do?

A: It is difficult to give a general answer to this question. Ask the Program Chair for guidance.

Q: Am I allowed to post my (non-blinded) paper on my web page? Can I advertise the unblinded version of my paper on mailing lists or send it to colleagues? Can I give a talk about my work while it is under review? How do I handle social media? What about arXiv?

A: We have developed guidelines, described here, to help everyone navigate in the same way the tension between (1) the normal communication of scientific results, which double-blind reviewing should not impede, and (2) actions that essentially force potential reviewers to learn the identity of the authors for a submission. Roughly speaking, you may (of course!) discuss work under submission, but you should not broadly advertise your work through media that is likely to reach your reviewers. We acknowledge there are grey areas and trade-offs; we cannot describe every possible scenario.

Things you may do:

  • Submit your paper to POPL, even if a previous version of it – under the same title or a different title – has been presented at an informal workshop, published on arXiv, or submitted to a previous conference or workshop.
  • Post your submission on your home page, your institutional repository, or arXiv, before or after the deadline (under whatever title you want).
  • Discuss your work with anyone who is not on the PC, or with PC members with whom you already have a conflict.
  • Present your work at professional meetings, informal workshops, or job interviews during the POPL review period.

The above is not an exhaustive list: when in doubt, ask the Program Chair.

Things you should not do:

  • Contact PC members (with whom you are not conflicted) about your work.
  • Publicize your work on major mailing lists used by the community (because potential reviewers likely read these lists).
  • Publicize your work on social media if wide public [re-]propagation is common (e.g., Twitter) and therefore likely to reach potential reviewers. For example, on Facebook, a post with a broad privacy setting (public or all friends) saying, “Whew, POPL paper in, time to sleep” is okay, but one describing the work or giving its title is not appropriate. Alternately, a post to a group including only the colleagues at your institution is fine.

Reviewers will not be asked to recuse themselves from reviewing your paper unless they feel you have gone out of your way to advertise your authorship information to them. If you are unsure about what constitutes “going out of your way”, please contact the Program Chair.

Q: Will the fact that POPL is double-blind have an impact on handling conflicts-of-interest?

A: Double-blind reviewing does not change the principle that reviewers should not review papers with which they have a conflict of interest, even if they do not immediately know who the authors are. Authors declare conflicts of interest when submitting their papers using the guidelines in the call for papers. Papers will not be assigned to reviewers who have a conflict.

For reviewers

Q: What should I do if I learn the authors’ identity? What should I do if a prospective POPL author contacts me and asks to visit my institution?

A: You should not treat double-blind reviewing differently from other reviewing. In particular, as explained above, it is fine for authors to give talks about their work (at workshops, job interviews, etc.), they cannot control who will attend their talks, and you as a PC member should not feel that you are prevented from attending their talks. Knowing (for whatever reason) that a paper was written by a certain author does not prevent you from reviewing the paper.

That said, if you feel that the authors’ actions are in flagrant violation of double-blind review, that is a point of concern. For example, if an author e-mails you their brand new POPL submission and asks to visit your institution to discuss it, that would clearly not be appropriate. There is a grey zone here, so use your best judgment, and when in doubt, ask the Program Chair how to proceed.

Q: The authors have provided a URL to supplemental material. I would like to see the material but I worry they will snoop my IP address and learn my identity. What should I do?

A: You are under no obligation to follow any URLs to external supplementary material. If the submission is not self contained and does not convince you by itself about its merits, then the paper should not be accepted. If you ever have reason to suspect that your anonymity was compromised through your following of a link, please share that information with the PC chair immediately, as this would constitute a breach of academic integrity on the part of the authors.

Q: If I am assigned a paper for which I feel I am not an expert, how do I seek an outside review?

A: PC members should do their own reviews, not delegate them to someone else. If doing so is problematic for some papers, e.g., you don’t feel completely qualified to review them, or if you know someone who would be the perfect reviewer for the paper, then bring this to the attention of the Associate Chair handling your paper, and discuss with them potential external reviewers (or other PC members) who might be able to provide an expert review. Then, submit a review for the paper that is as careful as possible, pointing out the areas where you think your knowledge is lacking. The Associate Chairs will manage the process of ensuring that papers receive sufficient expert reviews; please do not contact outside reviewers yourself.

Q: How do we handle potential conflicts of interest since I cannot see the author names?

A: The conference review system will ask that you identify conflicts of interest when you get an account on the submission system. It is critical that you enter these at least a week before the POPL submission deadline. Feel free to also identify additional authors whose papers you feel you could not review fairly for reasons other than those given (e.g., strong personal friendship).

Q: How should I avoid learning the authors’ identity if I am using web-search in the process of performing my review?

A: You should make a good-faith effort not to find the authors’ identity during the review period, but if you inadvertently do so, this does not disqualify you from reviewing the paper. As part of the good-faith effort, avoid using search engines with terms like the paper’s title or the name of a new system being discussed.


These guidelines are largely based on guidelines for POPL 2023, with a few modifications by Derek Dreyer based on discussions with the POPL Steering Committee. The earlier guidelines evolved from guidelines used at POPL and PLDI for a number of years, which originated in guidelines created by Mike Hicks for POPL 2012.