This program is tentative and subject to change.
Wed 14 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:00 | |||
09:00 60mKeynote | Medium-scale automation for proof assistants POPL Damien Pous CNRS | ||
10:30 - 12:10 | |||
10:30 25mTalk | A Modular Static Cost Analysis for GPU Warp-Level Parallelism POPL Gregory Blike University of Massachusetts at Boston, Hannah Zicarelli University of Massachusetts at Boston, Udaya Sathiyamoorthy University of Massachusetts at Boston, Julien Lange Royal Holloway University of London, Tiago Cogumbreiro University of Massachusetts at Boston DOI | ||
10:55 25mTalk | ChiSA: Static Analysis for Lightweight Chisel Verification POPL Jiacai Cui Nanjing University, Qinlin Chen Nanjing University, Zhongsheng Zhan Nanjing University, Tian Tan Nanjing University, Yue Li Nanjing University DOI | ||
11:20 25mTalk | Miri: Practical Undefined Behavior Detection for Rust POPL Ralf Jung ETH Zurich, Benjamin Kimock Lansweeper NV, Christian Poveda Unaffiliated, Eduardo Sánchez Muñoz Unaffiliated, Oli Scherer Unaffiliated, Qian (Andy) Wang ETH Zurich and Imperial College London DOI | ||
11:45 25mTalk | Piecewise Analysis of Probabilistic Programs via k-Induction POPL Tengshun Yang Institute of Software at Chinese Academy of Sciences, Shenghua Feng Institute of Software at Chinese Academy of Sciences, Hongfei Fu Shanghai Jiao Tong University, Naijun Zhan Peking University; Zhongguancun Lab, Jingyu Ke Shanghai Jiao Tong University, Shiyang Wu Shanghai Jiao Tong University DOI | ||
10:30 - 12:10 | |||
10:30 25mTalk | Domain-Theoretic Semantics for Functional Logic Programming POPL Eddie Jones University of Bristol, Samson Main University of Bristol, Celia Mengyue Li University of Bristol, Jonathan Marriott University of Bristol, Alex Kavvos University of Bristol DOI | ||
10:55 25mTalk | Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks POPL Michael Lee University of Cambridge, UK, Ningning Xie University of Toronto, Oleg Kiselyov Tohoku University, Jeremy Yallop University of Cambridge DOI | ||
11:20 25mTalk | Hyperfunctions: Communicating Continuations POPL DOI Pre-print | ||
11:45 25mTalk | Lazy Linearity for a Core Functional Language POPL DOI | ||
10:30 - 12:10 | |||
10:30 25mTalk | Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures POPL C. Aiswarya Chennai Mathematical Institute, Pascal Baumann MPI-SWS, Prakash Saivasan Institute of Mathematical Sciences, Lia Schütze MPI-SWS, Georg Zetzsche MPI-SWS DOI | ||
10:55 25mTalk | Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications POPL Aurèle Barrière EPFL, Victor Deng EPFL; École Normale Supérieure - PSL - CNRS, Clément Pit-Claudel EPFL DOI | ||
11:20 25mTalk | Network Change Validation with Relational NetKAT POPL Han Xu Princeton University, Zachary Kincaid Princeton University, Ratul Mahajan University of Washington, Intentionet, David Walker DOI | ||
11:45 25mTalk | Parameterized Verification of Quantum Circuits POPL Parosh Aziz Abdulla Uppsala University; Mälardalen University, Yu-Fang Chen Academia Sinica, Michal Hečko Brno University of Technology, Lukáš Holík Brno University of Technology; Aalborg University, Ondřej Lengál Brno University of Technology, Jyun-Ao Lin National Taipei University of Technology, Ramanathan S. Thinniyam Uppsala University DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | An Expressive Assertion Language for Quantum Programs POPL Bonan Su Tsinghua University, Yuan Feng Tsinghua University, Mingsheng Ying Institute of Software at Chinese Academy of Sciences; Tsinghua University, Li Zhou Institute of Software at Chinese Academy of Sciences DOI | ||
14:25 25mTalk | Hadamard-Pi: Equational Quantum Programming POPL Wang Fang University of Edinburgh, Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark DOI | ||
14:50 25mTalk | Qudit Quantum Programming with Projective Cliffords POPL DOI | ||
15:15 25mTalk | RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing POPL Yusuke Matsushita Kyoto University, Kengo Hirata University of Edinburgh, Ryo Wakizaka Kyoto University, Emanuele D'Osualdo University of Konstanz DOI Pre-print | ||
14:00 - 15:40 | |||
14:00 25mTalk | Extensible Data Types with Ad-Hoc Polymorphism POPL Matthew Toohey University of Toronto, Yanning Chen University of Toronto, Ara Jamalzadeh University of Toronto, Ningning Xie University of Toronto DOI | ||
14:25 25mTalk | Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems POPL Joseph Zullo Purdue University DOI | ||
14:50 25mTalk | Local Contextual Type Inference POPL Xu Xue University of Hong Kong, Chen Cui University of Hong Kong, Shengyi Jiang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI | ||
15:15 25mTalk | Typing Strictness POPL Daniel Sainati University of Pennsylvania, Joseph W. Cutler University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Stephanie Weirich University of Pennsylvania DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | Characterizing Sets of Theories That Can Be Disjointly Combined POPL DOI | ||
16:35 25mTalk | Context-Free-Language Reachability for Almost-Commuting Transition Systems POPL Nikhil Pimpalkhare Princeton University, Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin-Madison DOI | ||
17:00 25mTalk | Determination Problems for Orbit Closures and Matrix Groups POPL Rida Ait El Manssour University of Oxford, George Kenison Liverpool John Moores University, Mahsa Shirmohammadi CNRS, Anton Varonka TU Wien, James Worrell University of Oxford DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages POPL Zhentao Ye Peking University, Ruyi Ji Peking University, Yingfei Xiong Peking University, Xin Zhang Peking University DOI | ||
16:35 25mTalk | Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling POPL Doyoon Lee Seoul National University, Woosuk Lee Hanyang University, Kwangkeun Yi Seoul National University DOI | ||
17:00 25mTalk | Oriented Metrics for Bottom-Up Enumerative Synthesis POPL DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models POPL Shaan Nagy University of California at San Diego, Timothy Zhou , Nadia Polikarpova University of California at San Diego, Loris D'Antoni University of California at San Diego DOI | ||
16:35 25mTalk | Compiling to Linear Neurons POPL Joey Velez-Ginorio , Nada Amin Harvard University, Konrad Kording University of Pennsylvania, Steve Zdancewic University of Pennsylvania DOI | ||
17:00 25mTalk | Fuzzing Guided by Bayesian Program Analysis POPL DOI | ||
Thu 15 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
10:20 - 12:00 | |||
10:20 25mTalk | (TOPLAS) Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection POPL | ||
10:45 25mTalk | Verifying Almost-Sure Termination for Randomized Distributed Algorithms POPL Constantin Enea LIX, CNRS, Ecole Polytechnique, Rupak Majumdar MPI-SWS, Harshit Jitendra Motwani MPI-SWS, V.R. Sathiyanarayana MPI-SWS DOI | ||
11:10 25mTalk | Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic POPL DOI | ||
11:35 25mTalk | The Complexity of Testing Message-Passing Concurrency POPL Zheng Shi National University of Singapore, Lasse Møldrup Aarhus University, Umang Mathur National University of Singapore, Andreas Pavlogiannis Aarhus University DOI Pre-print | ||
10:20 - 12:00 | |||
10:20 25mTalk | A Relational Separation Logic for Effect Handlers POPL Paulo Emílio de Vilhena Imperial College London, Simcha van Collem Radboud University Nijmegen, Ines Wright Aarhus University, Robbert Krebbers Radboud University Nijmegen DOI | ||
10:45 25mTalk | Bayesian Separation Logic POPL Shing Hin Ho Imperial College London, Nicolas Wu Imperial College London, Azalea Raad Imperial College London DOI | ||
11:10 25mTalk | Cryptis: Cryptographic Reasoning in Separation Logic POPL Arthur Azevedo de Amorim Rochester Institute of Technology, Amal Ahmed Northeastern University, USA, Marco Gaboardi Boston University DOI | ||
11:35 25mTalk | Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions POPL Neta Elad Tel Aviv University, Adithya Murali University of Wisconsin, Sharon Shoham Tel Aviv University DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | Classical Notions of Computation and the Hasegawa-Thielecke Theorem POPL Éléonore Mangel Univ. Paris Cité - CNRS - Inria, Paul-André Melliès Univ. Paris Cité - CNRS - Inria, Guillaume Munch-Maccagnoni Inria - LS2N - CNRS DOI | ||
14:25 25mTalk | From Semantics to Syntax: A Type Theory for Comprehension Categories POPL Niyousha Najmaei École Polytechnique, Niels van der Weide Radboud University, Benedikt Ahrens Delft University of Technology, Paige Randall North Utrecht University DOI | ||
14:50 25mTalk | Higher-Order Behavioural Conformances via Fibrations POPL Henning Urbat Friedrich-Alexander-University Erlangen-Nürnberg DOI | ||
15:15 25mTalk | What Is a Monoid? POPL DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | A Lazy, Concurrent Convertibility Checker POPL DOI | ||
14:25 25mTalk | Canonicity for Indexed Inductive-Recursive Types POPL András Kovács University of Gothenburg and Chalmers University of Technology DOI | ||
14:50 25mTalk | Coco: Corecursion with Compositional Heterogeneous Productivity POPL Jaewoo Kim Seoul National University, Yeonwoo Nam Seoul National University, Chung-Kil Hur Seoul National University DOI | ||
15:15 25mTalk | Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation POPL Marcus Rossel Barkhausen Institut; TU Darmstadt, Rudi Schneider TU Berlin, Thomas Koehler ICube Lab - CNRS - Université de Strasbourg, Michel Steuwer TU Berlin, Andrés Goens TU Darmstadt DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | A Logic for the Imprecision of Abstract Interpretations POPL Marco Campion Inria Paris - ENS - Université PSL, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Arizona, Caterina Urban Inria Paris - ENS - Université PSL DOI | ||
14:25 25mTalk | Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment POPL David M. Kahn Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University, Runming Li Carnegie Mellon University DOI | ||
14:50 25mTalk | JAX Autodiff from a Linear Logic Perspective POPL DOI | ||
15:15 25mTalk | U-Turn: Enhancing Incorrectness Analysis by Reversing Direction POPL Flavio Ascari University of Konstanz, Roberto Bruni University of Pisa, Roberta Gori Diaprtimento di Informatica, Universita' di Pisa, Italy, Azalea Raad Imperial College London DOI | ||
16:10 - 17:00 | |||
16:10 25mTalk | Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers POPL Xuanyu Peng University of California at San Diego, Dominic Kennedy University of Utah, Yuyou Fan University of Utah, Ben Greenman University of Utah, USA, John Regehr University of Utah, Loris D'Antoni University of California at San Diego DOI | ||
16:35 25mTalk | Parameterized Infinite-State Reactive Synthesis POPL DOI | ||
16:10 - 17:00 | |||
16:10 25mTalk | A Family of Sims with Diverging Interests POPL Nicolas Chappe CNRS - Verimag DOI | ||
16:35 25mTalk | Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation POPL Niklas Mück MPI-SWS, Aina Linn Georges Max Planck Institute for Software Systems (MPI-SWS), Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS, Michael Sammler Institute of Science and Technology Austria DOI | ||
16:10 - 17:00 | |||
16:10 25mTalk | Dependent Coeffects for Local Sensitivity Analysis POPL Victor Sannier Univ. Lille - CNRS - Inria - Centrale Lille - UMR 9189 CRIStAL, Patrick Baillot Univ. Lille - CNRS - Inria - Centrale Lille - UMR 9189 CRIStAL DOI | ||
16:35 25mTalk | Security Reasoning via Substructural Dependency Tracking POPL Hemant Gouni Carnegie Mellon University, Frank Pfenning Carnegie Mellon University, USA, Jonathan Aldrich Carnegie Mellon University DOI Pre-print | ||
Fri 16 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:00 | |||
09:00 60mKeynote | Hardware-Software Contracts for High Assurance with Applications to Side-Channel Security POPL Caroline Trippel Stanford University | ||
10:30 - 12:10 | |||
10:30 25mTalk | Abstraction Functions as Types POPL Harrison Grodin Carnegie Mellon University, Runming Li Carnegie Mellon University, Robert Harper Carnegie Mellon University DOI | ||
10:55 25mTalk | Foundational Multi-Modal Program Verifiers POPL Vladimir Gladshtein , George Pîrlea National University of Singapore, Qiyuan Zhao National University of Singapore, Vitaly Kurin Neapolis University Pafos, Ilya Sergey National University of Singapore DOI | ||
11:20 25mTalk | Stateful Differential Operators for Incremental Computing POPL DOI | ||
11:45 25mTalk | The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs POPL Frank Schüssele University of Freiburg, Matthias Zumkeller University of Freiburg, Miriam Lagunes-Rochin University of Freiburg, Dominik Klumpp LIX - CNRS - École Polytechnique; University of Freiburg DOI | ||
10:30 - 12:10 | |||
10:30 25mTalk | Di- is for Directed: First-Order Directed Type Theory via Dinaturality POPL Andrea Laretto Tallinn University of Technology, Fosco Loregian Tallinn University of Technology, Niccolò Veltri IT University of Copenhagen DOI | ||
10:55 25mTalk | Quotient Polymorphism POPL DOI | ||
11:20 25mTalk | The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types POPL Chun Yin Chau HKUST (The Hong Kong University of Science and Technology), Lionel Parreaux Hong Kong University of Science and Technology DOI | ||
11:45 25mTalk | Welterweight Go: Boxing, Structural Subtyping, and Generics POPL Raymond Hu Queen Mary University of London, Julien Lange Royal Holloway University of London, Bernardo Toninho Instituto Superior Técnico - University of Lisbon, Philip Wadler University of Edinburgh, Robert Griesemer Google, Keith Randall Google DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on Finite Relations, Labelled Posets, and Parameterized Algebraic Theories POPL Ohad Kammar University of Edinburgh, Jack Liell-Cock University of Oxford, Sam Lindley University of Edinburgh, Cristina Matache University of Edinburgh, Sam Staton University of Oxford DOI | ||
14:25 25mTalk | Handling Higher-Order Effectful Operations with Judgemental Monadic Laws POPL DOI | ||
14:50 25mTalk | Rows and Capabilities as Modal Effects POPL DOI | ||
15:15 25mTalk | The Relative Monadic Metalanguage POPL Jack Liell-Cock University of Oxford, Zev Shirazi University of Oxford, Sam Staton University of Oxford DOI | ||
14:00 - 15:40 | |||
14:00 25mTalk | AdapTT: Functoriality for Dependent Type Casts POPL Arthur Adjedj ENS Paris Saclay, Université Paris-Saclay, Meven Lennon-Bertrand Inria – Université Paris Cité, Thibaut Benjamin Université Paris-Saclay, CEA, List, Kenji Maillard Inria DOI | ||
14:25 25mTalk | Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach POPL DOI | ||
14:50 25mTalk | Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally POPL DOI | ||
15:15 25mTalk | Normalisation for First-Class Universe Levels POPL Nils Anders Danielsson University of Gothenburg, Naïm Camille Favier Chalmers University of Technology and University of Gothenburg, Ondřej Kubánek Chalmers University of Technology DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | A Complementary Approach to Incorrectness Typing POPL Celia Mengyue Li University of Bristol, Sophie Pull University of Bristol, Steven Ramsay University of Bristol DOI | ||
16:35 25mTalk | A Synthetic Reconstruction of Multiparty Session Types POPL David Castro-Perez University of Kent, Francisco Ferreira Royal Holloway, University of London, Sung-Shik Jongmans University of Groningen DOI | ||
17:00 25mTalk | Bounded Sort Polymorphism with Elimination Constraints POPL Johann Rosain ENS Lyon, Tomás Diaz University of Chile, Kenji Maillard Inria, Matthieu Sozeau Inria, Nicolas Tabareau Inria, Éric Tanter University of Chile, Théo Winterhalter INRIA DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | Counting and Sampling Traces in Regular Languages POPL Alexis de Colnet TU Wien, Kuldeep S. Meel University of Toronto, Umang Mathur National University of Singapore DOI Pre-print | ||
16:35 25mTalk | Parametrised Verification of Intel-x86 Programs POPL Parosh Aziz Abdulla Uppsala University; Mälardalen University, Mohamed Faouzi Atig Uppsala University, Ahmed Bouajjani Université Paris Cité, K Narayan Kumar Chennai Mathematical Institute, Prakash Saivasan Institute of Mathematical Sciences DOI | ||
17:00 25mTalk | General Decidability Results for Systems with Continuous Counters POPL A. R. Balasubramanian Technical University of Munich, Matthew Hague Royal Holloway University of London, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Uppsala University, Georg Zetzsche MPI-SWS DOI | ||
16:10 - 17:25 | |||
16:10 25mTalk | Generating Compilers for Qubit Mapping and Routing POPL Abtin Molavi University of Wisconsin-Madison, Amanda Xu University of Wisconsin-Madison, Ethan Cecchetti University of Wisconsin-Madison, Swamit Tannu University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison DOI | ||
16:35 25mTalk | On Circuit Description Languages, Indexed Monads, and Resource Analysis POPL Ken Sakayori University of Tokyo, Andrea Colledan University of Bologna; Centre Inria d’Université Côte d’Azur, Ugo Dal Lago University of Bologna; Centre Inria d’Université Côte d’Azur DOI | ||
17:00 25mTalk | Quantum Circuits Are Just a Phase POPL Chris Heunen University of Edinburgh, Louis Lemonnier University of Edinburgh, Christopher McNally Massachusetts Institute of Technology, Alex Rice University of Edinburgh DOI | ||
Unscheduled Events
| Not scheduled Meeting | PC Chair's Report and Business Meeting POPL |
Accepted Papers
POPL 2026 Call for Papers
PACMPL Issue POPL 2026 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 2026, 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 2026 will use a full double-blind reviewing process (similar to the one used in recent years (POPL 2023 - 2025) but different from the lightweight double-blind process used before then). 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, and there is no option to submit non-anonymized 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
POPL 2026 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 2026, policies specified in this Call for Papers supersede those in the Principles of POPL document.
Submission Site Information
The submission site is https://popl26.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 10, 2025 anywhere on earth (AoE): 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.
If a possible reviewer does not meet the above criteria, please do not identify him/her as conflicted. Doing so could be viewed as an attempt to prevent a qualified, but possibly skeptical reviewer from reviewing your paper. If you nevertheless believe that a reviewer who does not meet the above criteria is conflicted, or if you are unsure about a possible conflict, you may identify the person and send a note to the PC Chair. Declaring a spurious conflict with the aim of excluding otherwise qualified reviewers can be grounds for desk rejection.
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
acmartLaTeX class withacmsmalloption). 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
reviewandscreenoptions in order to make submissions easier to review. -
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 and Associate Chairs (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, 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 to give a short talk (roughly 25 minutes long) at the conference, according to the conference schedule. Authors who wish to present but who cannot attend in person will be provided with some option for remote presentation, as well as some mechanism for remote interaction with conference participants.
Important update on ACM’s new open access publishing model for 2026 ACM Conferences!
Starting January 1, 2026, ACM will fully transition to Open Access. All ACM publications, including those from ACM-sponsored conferences, will be 100% Open Access. Authors will have two primary options for publishing Open Access articles with ACM: the ACM Open institutional model or by paying Article Processing Charges (APCs). With over 1,800 institutions already part of ACM Open, the majority of ACM-sponsored conference papers will not require APCs from authors or conferences (currently, around 70-75%).
Authors from institutions not participating in ACM Open will need to pay an APC to publish their papers, unless they qualify for a financial or discretionary waiver. To find out whether an APC applies to your article, please consult the list of participating institutions in ACM Open and review the APC Waivers and Discounts Policy. Keep in mind that waivers are rare and are granted based on specific criteria set by ACM.
Understanding that this change could present financial challenges, ACM has approved a temporary subsidy for 2026 to ease the transition and allow more time for institutions to join ACM Open. The subsidy will offer: $250 APC for ACM/SIG members and $350 for non-members.
This represents a 65% discount, funded directly by ACM. Authors are encouraged to help advocate for their institutions to join ACM Open during this transition period.
This temporary subsidized pricing will apply to all conferences scheduled for 2026.
Distinguished Paper Awards
At most 10% of the accepted papers of POPL 2026 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.
Accepted Papers
The Complexity of Testing Message-Passing Concurrency
Zheng Shi, Lasse Møldrup, Umang Mathur, Andreas Pavlogiannis
Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-kinded Type Systems
Joseph A. Zullo
Normalisation for First-Class Universe Levels
Nils Anders Danielsson, Naïm Camille Favier, Ondřej Kubánek
Qudit Quantum Programming with Projective Cliffords
Jennifer Paykin, Sam Winnick
Hadamard-Pi: Equational Quantum Programming
Wang Fang, Chris Heunen, Robin Kaarsgaard
RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
Yusuke Matsushita, Kengo Hirata, Ryo Wakizaka, Emanuele D’Osualdo
Hyperfunctions: Communicating Continuations
Donnacha Oisín Kidney, Nicolas Wu
ArchSem: Reusable rigorous semantics of relaxed architectures
Thibaut Pérami, Thomas Bauereiss, Brian Campbell, Zongyuan Liu, Nils Lauermann, Alasdair Armstrong, Peter Sewell
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
Noam Zilberstein, Alexandra Silva, Joseph Tassarotti
Characterizing sets of theories that can be disjointly combined
Benjamin Przybocki, Guilherme V. Toledo, Yoni Zohar
Local Contextual Type Inference
Xu Xue, Chen Cui, Shengyi Jiang, Bruno C. d. S. Oliveira
JAX Autodiff from a Linear Logic Perspective
Giulia Giusti, Michele Pagani
TypeDis: A Type System for Disentanglement
Alexandre Moine, Stephanie Balzer, Alex Xu, Sam Westrick
Network Change Validation with Relational NetKAT
Han Xu, David Walker, Ratul Mahajan, Zachary Kincaid
Typing Strictness
Daniel Sainati, Joseph W. Cutler, Benjamin C. Pierce, Stephanie Weirich
An Expressive Assertion Language for Quantum Programs
Bonan Su, Yuan Feng, Mingsheng Ying, Li Zhou
Fuzzing Guided by Bayesian Program Analysis
Yifan Zhang, Xin Zhang
ChiSA: Static Analysis for Lightweight Chisel Verification
Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan, Yue Li
General Decidability Results for Systems with Continuous Counters
A. R. Balasubramanian, Matthew Hague, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche
Extensible Data Types with Ad-Hoc Polymorphism
Matthew Toohey, Yanning Chen, Ara Jamalzadeh, Ningning Xie
Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation
Sangho Lim, Hyoungjin Lim, Wonyeol Lee, Xavier Rival, Hongseok Yang
AdapTT: Functoriality for Dependent Type Casts
Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, Kenji Maillard
Quotient Polymorphism
Brandon Hewer, Graham Hutton
On Circuit Description Languages, Indexed Monads, and Resource Analysis
Ken Sakayori, Andrea Colledan, Ugo Dal Lago
Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation
Marcus Rossel, Rudi Schneider, Thomas Koehler, Michel Steuwer, Andrés Goens
All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs
Alexandre Moine, Sam Westrick, Joseph Tassarotti
Security Reasoning via Substructural Dependency Tracking
Hemant Gouni, Frank Pfenning, Jonathan Aldrich
Dependent Coeffects for Local Sensitivity Analysis
Victor Sannier, Patrick Baillot
Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
Neta Elad, Adithya Murali, Sharon Shoham
Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach
Yiyun Liu, Stephanie Weirich
Abstraction Functions as Types
Harrison Grodin, Runming Li, Robert Harper
Rows and Capabilities as Modal Effects
Wenhao Tang, Sam Lindley
Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages
Davide Barbarossa, Paolo Pistone
A Relational Separation Logic for Effect Handlers
Paulo Emílio de Vilhena, Simcha van Collem, Ines Wright, Robbert Krebbers
Compiling to linear neurons
Joey Velez-Ginorio, Nada Amin, Konrad Kording, Steve Zdancewic
Handlers of Higher-Order Effectful Operations
Zhixuan Yang, Nicolas Wu
Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages
Zhentao Ye, Ruyi Ji, Yingfei Xiong, Xin Zhang
Parametrised Verification of Intel-x86 programs
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K Narayan Kumar, Prakash Saivasan
Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks
Michael Lee, Ningning Xie, Oleg Kiselyov, Jeremy Yallop
Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic Back-Translation
Niklas Mück, Aïna Linn Georges, Derek Dreyer, Deepak Garg, Michael Sammler
Arbitration-Free Consistency is Available (and Vice Versa)
Hagit Attiya, Constantin Enea, Enrique Román-Calvo
The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs
Frank Schüssele, Matthias Zumkeller, Miriam Lagunes-Rochin, Dominik Klumpp
Canonicity for Indexed Inductive-Recursive Types
András Kovács
Context-Free-Language Reachability for Almost-Commuting Transition Systems
Nikhil Pimpalkhare, Zachary Kincaid, Thomas Reps
Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
Thomas Haas, Roland Meyer, Hernán Ponce de León, Andrés Lomeli
U-Turn: Enhancing Incorrectness Analysis by Reversing Direction
Flavio Ascari, Roberto Bruni, Roberta Gori, Azalea Raad
The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-recursive Types
Chun Yin Chau, Lionel Parreaux
Miri: Practical Undefined Behavior Detection for Rust
Ralf Jung, Benjamin Kimock, Christian Poveda, Eduardo Sánchez Muñoz, Oli Scherer, Qian Wang
Verifying Almost-Sure Termination for Randomized Distributed Algorithms
Constantin Enea, Rupak Majumdar, Harshit Jitendra Motwani, V. R. Sathiyanarayana
A Synthetic Reconstruction of Multiparty Session Types
David Castro-Perez, Francisco Ferreira, Sung-Shik Jongmans
A Modular Static Cost Analysis For GPU Warp-Level Parallelism
Gregory Blike, Hannah Zicarelli, Udaya Sathiyamoorthy, Julien Lange, Tiago Cogumbreiro
Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling
Doyoon Lee, Woosuk Lee, Kwangkeun Yi
A Lazy, Concurrent Convertibility Checker
Nathanaëlle Courant, Xavier Leroy
Bayesian Separation Logic
Shing Hin Ho, Nicolas Wu, Azalea Raad
Higher-Order Behavioural Conformances via Fibrations
Henning Urbat
Determination Problems for Orbit Closures and Matrix Groups
Rida Ait El Manssour, George Kenison, Mahsa Shirmohammadi, Anton Varonka, James Worrell
Domain-theoretic Semantics for Functional Logic Programming
Eddie Jones, Samson Main, Celia Mengyue Li, Jonathan Marriott, G. A. Kavvos
Consistent Updates for Scalable Microservices
Devora Chait-Roth, Kedar Namjoshi, Thomas Wies
Zoo: A framework for the verification of concurrent OCaml 5 programs using separation logic
Clément Allain, Gabriel Scherer
The Relative Monadic Metalanguage
Jack Liell-Cock, Zev Shirazi, Sam Staton
Di- is for Directed: First-Order Directed Type Theory via Dinaturality
Andrea Laretto, Fosco Loregian, Niccolò Veltri
Encode the Cake and Eat it Too: Controlling computation in type theory, locally
Yann Leray, Théo Winterhalter
DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
Aleksandr Fedchin, Antero Mejr, Hari Sundar, Jeffrey S. Foster
An Equational Axiomatization of Dynamic Threads via Algebraic Effects
Ohad Kammar, Jack Liell-Cock, Sam Lindley, Cristina Matache, Sam Staton
A Logic for the Imprecision of Abstract Interpretations
Marco Campion, Mila Dalla Preda, Roberto Giacobazzi, Caterina Urban
ChopChop: a Programmable Framework for Semantically Constraining the Output of Language Models
Shaan Nagy, Timothy Zhou, Nadia Polikarpova, Loris D’Antoni
Piecewise Analysis of Probabilistic Programs via k-Induction
Tengshun Yang, Shenghua Feng, Hongfei Fu, Naijun Zhan, Jingyu Ke, Shiyang Wu
Formal Verification for JavaScript Regular Expressions: a Proven Mechanized Semantics and its Applications
Aurèle Barrière, Victor Deng, Clément Pit-Claudel
Lazy Linearity for a Core Functional Language
Rodrigo Mesquita, Bernardo Toninho
Parameterized Verification of Quantum Circuits
Parosh Aziz Abdulla, Yu-Fang Chen, Michal Hečko, Lukáš Holík, Ondřej Lengál, Jyun-Ao Lin, Ramanathan Thinniyam Srinivasan
A Verified High-Performance Composable Object Library for Remote Direct Memory Access
Guillaume Ambal, George Hodgkins, Mark Madler, Gregory Chockler, Brijesh Dongol, Joseph Izraelevitz, Azalea Raad, Viktor Vafeiadis
A Family of Sims with Diverging Interests
Nicolas Chappe
Classical notions of computation and the Hasegawa-Thielecke theorem
Éléonore Mangel, Paul-André Melliès, Guillaume Munch-Maccagnoni
Bounded treewidth, multiple context-free grammars, and downward closures
C. Aiswarya, Pascal Baumann, Prakash Saivasan, Lia Schütze, Georg Zetzsche
Oriented Metrics for Bottom-Up Enumerative Synthesis
Roland Meyer, Jakob Tepe
Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
David M. Kahn, Jan Hoffmann, Runming Li
Foundational Multi-Modal Program Verifiers
Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, Ilya Sergey
Generating Compilers for Qubit Mapping and Routing
Abtin Molavi, Amanda Xu, Ethan Cecchetti, Swamit Tannu, Aws Albarghouthi
Welterweight Go: Boxing, Structural Subtyping and Generics
Raymond Hu, Julien Lange, Bernardo Toninho, Philip Wadler, Robert Griesemer, Keith Randall
Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
Xuanyu Peng, Dominic Kennedy, Yuyou Fan, Ben Greenman, John Regehr, Loris D’Antoni
Counting and Sampling Traces in Regular Languages
Alexis de Colnet, Kuldeep S. Meel, Umang Mathur
A Complementary Approach to Incorrectness Typing
Celia Mengyue Li, Sophie Pull, Steven Ramsay
From Semantics to Syntax: A Type Theory for Comprehension Categories
Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens, Paige Randall North
Parameterized Infinite-State Reactive Synthesis
Benedikt Maderbacher, Roderick Bloem
What is a Monoid?
Morgan Rogers, Paul Blain Levy
Stateful Differential Operators for Incremental Computing
Runqing Xu, Sebastian Erdweg
Probabilistic Programming with Vectorized Programmable Inference
McCoy Becker, Mathieu Huot, George Matheos, Xiaoyan Wang, Karen Chung, Colin Smith, Sam Ritchie, Rif A. Saurous, Alexander K. Lew, Martin Rinard, Vikash K. Mansinghka
Cryptis: Cryptographic Reasoning in Separation Logic
Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi
Quantum circuits are just a phase
Chris Heunen, Louis Lemonnier, Christopher McNally, Alex Rice
Bounded Sort Polymorphism with Elimination Constraints
Johann Rosain, Tomás Díaz, Kenji Maillard, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter, Théo Winterhalter
Coco: Corecursion with Compositional Heterogeneous Productivity
Jaewoo Kim, Yeonwoo Nam, Chung-Kil Hur
FAQ on Double-Blind Reviewing
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.