POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Dates
You're viewing the program in a time zone which is different from your device's time zone change time zone

Wed 17 Jan

Displayed time zone: London change

08:50 - 09:00
Welcome from the ChairPOPL at Kelvin Lecture +0min
08:50 - 09:00
Welcome from the ChairPOPL at Turing Lecture
09:00 - 10:00
Keynote 1POPL at Kelvin Lecture
Chair(s): Derek Dreyer MPI-SWS
09:00
60m
Talk
A New Perspective on Commutativity in Verification
POPL
Azadeh Farzan University of Toronto
10:30 - 11:50
Synthesis 1POPL at Kelvin Lecture
Chair(s): Soham Chakraborty TU Delft
10:30
20m
Talk
Implementation and Synthesis of Math Library FunctionsDistinguished Paper
POPL
Ian Briggs University of Utah, Yash Lad University of Utah, Pavel Panchekha University of Utah
10:50
20m
Talk
Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations
POPL
Yuantian Ding Purdue University, Xiaokang Qiu Purdue University
11:10
20m
Talk
Efficient Bottom-Up Synthesis for Programs with Local Variables
POPL
Xiang Li University of Michigan, Ann Arbor, Xiangyu Zhou University of Michigan, Rui Dong University of Michigan, Yihong Zhang University of Washington, Xinyu Wang University of Michigan
Pre-print
11:30
20m
Talk
Optimal Program Synthesis via Abstract Interpretation
POPL
Stephen Mell University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Osbert Bastani University of Pennsylvania
10:30 - 11:50
Types 1POPL at Turing Lecture
Chair(s): Mae Milano Princeton University
10:30
20m
Talk
Generating Well-Typed Terms that are not "Useless"
POPL
Justin Frank University of Maryland, College Park, Benjamin Quiring University of Maryland, Leonidas Lampropoulos University of Maryland, College Park
10:50
20m
Talk
Indexed Types for a Statically Safe WebAssembly
POPL
Adam Geller Computer Science, University of British Columbia, Justin Frank University of Maryland, College Park, William J. Bowman University of British Columbia
DOI Pre-print
11:10
20m
Talk
The Essence of Generalized Algebraic Data TypesRemote
POPL
Filip Sieczkowski Heriot-Watt University, Sergei Stepanenko Aarhus University, Jonathan Sterling University of Cambridge, Lars Birkedal Aarhus University
11:30
20m
Talk
Ill-Typed Programs Don't Evaluate
POPL
Steven Ramsay University of Bristol, Charlie Walpole University of Bristol
13:20 - 14:40
Effect HandlersPOPL at Kelvin Lecture
Chair(s): Cătălin Hriţcu MPI-SP
13:20
20m
Talk
Soundly Handling LinearityDistinguished Paper
POPL
Wenhao Tang University of Edinburgh, Daniel Hillerström Huawei Zurich Research Center, Sam Lindley University of Edinburgh, J. Garrett Morris University of Iowa
DOI Pre-print
13:40
20m
Talk
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers
POPL
Fuga Kawamata Waseda University, Hiroshi Unno University of Tsukuba, Taro Sekiyama National Institute of Informatics, Tachio Terauchi Waseda University
14:00
20m
Talk
Effectful Software Contracts
POPL
Cameron Moy Northeastern University, Christos Dimoulas Northwestern University, Matthias Felleisen Northeastern University
14:20
20m
Talk
Algebraic Effects Meet Hoare Logic in Cubical Agda
POPL
Oisín Kidney Imperial College London, Zhixuan Yang Imperial College London, Nicolas Wu Imperial College London
Pre-print
13:20 - 14:40
Automated VerificationPOPL at Turing Lecture
Chair(s): Gregory Malecha BedRock Systems
13:20
20m
Talk
Regular Abstractions for Array Systems
POPL
Chih-Duo Hong National Chengchi University, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS
13:40
20m
Talk
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive VerificationDistinguished Paper
POPL
Neta Elad Tel Aviv University, Oded Padon VMware Research, Sharon Shoham Tel Aviv University
Link to publication DOI
14:00
20m
Talk
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking FunctionsRemote
POPL
Jianan Yao Columbia University, Runzhou Tao Columbia University, Ronghui Gu Columbia University, Jason Nieh Columbia University
14:20
20m
Talk
Decision and Complexity of Dolev-Yao Hyperproperties
POPL
Itsaka Rakotonirina MPI-SP, Gilles Barthe MPI-SP; IMDEA Software Institute, Clara Schneidewind MPI-SP
15:10 - 16:30
Automata And ComplexityPOPL at Kelvin Lecture
Chair(s): Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital
15:10
20m
Talk
Parikh's Theorem Made Symbolic
POPL
Matthew Hague Royal Holloway University of London, Artur Jez University of Wroclaw, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS
15:30
20m
Talk
Efficient Matching of Regular Expressions with Lookaround Assertions
POPL
Konstantinos Mamouras Rice University, Agnishom Chattopadhyay Rice University
15:50
20m
Talk
The Complex(ity) Landscape of Checking Infinite Descent
POPL
Liron Cohen Ben-Gurion University of the Negev, Adham Jabarin Ben Gurion University, Andrei Popescu University of Sheffield, Reuben N. S. Rowe Royal Holloway University of London
16:10
20m
Talk
Positive Almost-Sure Termination – Complexity and Proof Rules
POPL
15:10 - 16:30
Separation LogicPOPL at Turing Lecture
Chair(s): Azalea Raad Imperial College London
15:10
20m
Talk
An Iris Instance for Verifying CompCert C Programs
POPL
William Mansky University of Illinois Chicago, Ke Du
Pre-print
15:30
20m
Talk
The Logical Essence of Well-Bracketed Control Flow
POPL
Amin Timany Aarhus University, Armaël Guéneau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, Lars Birkedal Aarhus University
15:50
20m
Talk
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
POPL
Simon Oddershede Gregersen Aarhus University, Alejandro Aguirre Aarhus University, Philipp G. Haselwarter Aarhus University, Joseph Tassarotti NYU, Lars Birkedal Aarhus University
DOI Pre-print
16:10
20m
Talk
Thunks and Debits in Separation Logic with Time Credits
POPL
François Pottier Inria, Armaël Guéneau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, Jacques-Henri Jourdan CNR, LMF, Glen Mével
16:50 - 18:10
ConcurrencyPOPL at Kelvin Lecture
Chair(s): Sophia Drossopoulou Imperial College London
16:50
20m
Talk
A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
POPL
Prasad Jayanti Department of Computer Science, Dartmouth College, USA, Siddhartha Jayanti Google Research, Ugur Y. Yavuz Boston University, Lizzie Hernandez Videa Microsoft
17:10
20m
Talk
Predictive Monitoring against Pattern Regular Languages
POPL
Zhendong Ang National University of Singapore, Umang Mathur National University of Singapore
Pre-print
17:30
20m
Talk
Commutativity Simplifies Proofs of Parameterized Programs
POPL
Azadeh Farzan University of Toronto, Dominik Klumpp University of Freiburg, Andreas Podelski University of Freiburg
Pre-print
17:50
20m
Talk
Coarser Equivalences for Causal Concurrency
POPL
Azadeh Farzan University of Toronto, Umang Mathur National University of Singapore
Pre-print
16:50 - 18:10
Domain-Specific LanguagesPOPL at Turing Lecture
Chair(s): Satnam Singh Groq
16:50
20m
Talk
EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
POPL
Pu Sun ShanghaiTech University, Fu Song State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, and University of Chinese Academy of Sciences Beijing, China, Yuqi Chen ShanghaiTech University, China, Taolue Chen University of London
17:10
20m
Talk
A Core Calculus for Documents: Or, Lambda: The Ultimate Document
POPL
Will Crichton Brown University, Shriram Krishnamurthi Brown University
Pre-print
17:30
20m
Talk
Validation of Modern JSON Schema: Formalization and Complexity
POPL
Lyes Attouche Université Paris-Dauphine -- PSL, Mohamed-Amine Baazizi Sorbonne Université, Dario Colazzo Université Paris-Dauphine -- PSL, Giorgio Ghelli Universita di Pisa, Carlo Sartiani Università della Basilicata, Stefanie Scherzinger Universität Passau
DOI
17:50
20m
Talk
Shoggoth - A Formal Foundation for Strategic Rewriting
POPL
Xueying Qin The University of Edinburgh, Liam O'Connor University of Edinburgh, Rob van Glabbeek The University of Edinburgh, Peter Hoefner Australian National University, Ohad Kammar University of Edinburgh, Michel Steuwer TU Berlin; University of Edinburgh
Pre-print
18:10 - 20:00
POPL Networking ReceptionPOPL at Maxwell Library
18:10
1h50m
Social Event
POPL Networking Reception
POPL

18:10 - 20:00
POPL Networking ReceptionPOPL at Riverside Room
18:10
1h50m
Social Event
POPL Networking Reception
POPL

Thu 18 Jan

Displayed time zone: London change

09:00 - 10:20
Synthesis 2POPL at Kelvin Lecture
Chair(s): Michael Hicks Amazon Web Services and the University of Maryland
09:00
20m
Talk
Semantic Code Refactoring for Abstract Data Types
POPL
Shankara Pailoor University of Texas at Austin, Yuepeng Wang Simon Fraser University, Işıl Dillig University of Texas at Austin
09:20
20m
Talk
API-driven Program Synthesis for Testing Static Typing Implementations
POPL
Thodoris Sotiropoulos ETH Zurich, Stefanos Chaliasos Imperial College London, Zhendong Su ETH Zurich
09:40
20m
Talk
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
POPL
Kevin Batz RWTH Aachen University, Tom Biskup RWTH Aachen University, Germany, Joost-Pieter Katoen RWTH Aachen University, Tobias Winkler RWTH Aachen University
10:00
20m
Talk
A Case for Synthesis of Recursive Quantum Unitary Programs
POPL
Haowei Deng University of Maryland at College Park, Runzhou Tao Columbia University, Yuxiang Peng University of Maryland, Xiaodi Wu University of Maryland
09:00 - 10:20
Higher-Order Effectful ProgramsPOPL at Turing Lecture
Chair(s): Sam Lindley University of Edinburgh
09:00
20m
Talk
On Model-Checking Higher-Order Effectful Programs
POPL
Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis, Alexis Ghyselen University of Bologna
09:20
20m
Talk
Explicit Effects and Effect Constraints in ReML
POPL
Martin Elsman University of Copenhagen, Denmark
Link to publication DOI
09:40
20m
Talk
Decalf: A Directed, Effectful Cost-Aware Logical Framework
POPL
Harrison Grodin , Jonathan Sterling University of Cambridge, Yue Niu Carnegie Mellon University, Robert Harper Carnegie Mellon University
Pre-print
10:00
20m
Talk
Modular Denotational Semantics for Effects with Guarded Interaction TreesDistinguished PaperRemote
POPL
Daniel Frumin University of Groningen, Amin Timany Aarhus University, Lars Birkedal Aarhus University
DOI Pre-print
10:50 - 12:10
Types 2POPL at Kelvin Lecture
Chair(s): Stefan K. Muller Illinois Institute of Technology
10:50
20m
Talk
Quotient Haskell: Lightweight Quotient Types for All
POPL
Brandon Hewer University of Nottingham, Graham Hutton University of Nottingham, UK
11:10
20m
Talk
Focusing on Refinement Typing (TOPLAS)Remote
POPL
Dimitrios Economou Queen's University, Canada, Neel Krishnaswami University of Cambridge, Jana Dunfield Queen's University, Kingston, Ontario
Link to publication
11:30
20m
Talk
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic ProgramsRemote
POPL
Guannan Wei Purdue University, Oliver Bračevac Galois, Inc., Songlin Jia Purdue University, USA, Yuyan Bao Augusta University, Tiark Rompf Purdue University
11:50
20m
Talk
Capturing Types (TOPLAS)
POPL
Aleksander Boruch-Gruszecki EPFL, Martin Odersky EPFL, Edward Lee University of Waterloo, Ondřej Lhoták University of Waterloo, Jonathan Immanuel Brachthäuser University of Tübingen
DOI File Attached
10:50 - 12:10
Probabilistic ProgramsPOPL at Turing Lecture
Chair(s): Jules Jacobs Radboud University Nijmegen
10:50
20m
Talk
Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
POPL
Nate Ackerman Harvard University, Cameron Freer Massachusetts Institute of Technology, Younesse Kaddar University of Oxford, Jacek Karwowski University of Oxford, Sean Moss University of Oxford, Daniel Roy University of Toronto, Sam Staton University of Oxford, Hongseok Yang KAIST; IBS
11:10
20m
Talk
Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
POPL
Francesca Randone IMT School for Advanced Studies Lucca, Luca Bortolussi Department of Mathematics and Geosciences, University of Trieste, Emilio Incerto IMT School for Advanced Studies Lucca, Mirco Tribastone IMT Institute for Advanced Studies Lucca, Italy
11:30
20m
Talk
Higher Order Bayesian Networks, Exactly
POPL
Claudia Faggian Université de Paris & CNRS, Daniele Pautasso Università di Torino, Gabriele Vanoni IRIF, Université Paris Cité
11:50
20m
Talk
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
POPL
13:40 - 15:00
Quantum ComputingPOPL at Kelvin Lecture
Chair(s): Oded Padon VMware Research
13:40
20m
Talk
With a Few Square Roots, Quantum Computing is as Easy as Pi
POPL
Jacques Carette McMaster University, Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark, Amr Sabry Indiana University
Pre-print
14:00
20m
Talk
Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-Deterministic Observers
POPL
Lorenzo Ceragioli IMT Lucca, Italy, Fabio Gadducci University of Pisa, Giuseppe Lomurno University of Pisa, Italy, Gabriele Tedeschi University of Pisa, Italy
14:20
20m
Talk
SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog CompilationRemote
POPL
Yuxiang Peng University of Maryland, Jacob Young University of Maryland, Pengyu Liu Tsinghua University, Xiaodi Wu University of Maryland
14:40
20m
Talk
Enriched Presheaf Model of Quantum FPC
POPL
Takeshi Tsukada Chiba University, Kazuyuki Asada Tohoku University
13:40 - 15:00
Weak Memory and Concurrent Separation LogicPOPL at Turing Lecture
Chair(s): William Mansky University of Illinois Chicago
13:40
20m
Talk
How Hard is Weak-Memory Testing?
POPL
Soham Chakraborty TU Delft, Shankaranarayanan Krishna IIT Bombay, India, Umang Mathur National University of Singapore, Andreas Pavlogiannis Aarhus University
Pre-print
14:00
20m
Talk
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
POPL
Angus Hammond University of Cambridge, Zongyuan Liu Aarhus University, Thibaut Pérami University of Cambridge, Peter Sewell University of Cambridge, Lars Birkedal Aarhus University, Jean Pichon-Pharabod Aarhus University
Pre-print
14:20
20m
Talk
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
POPL
Amin Timany Aarhus University, Simon Oddershede Gregersen Aarhus University, Leo Stefanesco MPI-SWS, Jonas Kastberg Hinrichsen Aarhus University, Denmark, Léon Gondelman Aarhus University, Abel Nieto Aarhus University, Lars Birkedal Aarhus University
14:40
20m
Talk
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
POPL
Jules Jacobs Radboud University Nijmegen, Jonas Kastberg Hinrichsen Aarhus University, Denmark, Robbert Krebbers Radboud University Nijmegen
Pre-print
15:30 - 16:50
ParallelismPOPL at Kelvin Lecture
Chair(s): John Reppy University of Chicago, USA
15:30
20m
Talk
Pipelines and Beyond: Graph Types for ADTs with Futures
POPL
Francis Rinaldi Illinois Institute of Technology, june wunder Boston University, Arthur Azevedo de Amorim Rochester Institute of Technology, USA, Stefan K. Muller Illinois Institute of Technology
15:50
20m
Talk
Disentanglement with Futures, State, and Interaction
POPL
Jatin Arora Carnegie Mellon University, Stefan K. Muller Illinois Institute of Technology, Umut A. Acar Carnegie Mellon University
16:10
20m
Talk
DisLog: A Separation Logic for Disentanglement
POPL
Alexandre Moine Inria, Sam Westrick Carnegie Mellon University, Stephanie Balzer Carnegie Mellon University
Pre-print
16:30
20m
Talk
Automatic Parallelism ManagementDistinguished Paper
POPL
Sam Westrick Carnegie Mellon University, Matthew Fluet Rochester Institute of Technology, Mike Rainey Carnegie Mellon University, Umut A. Acar Carnegie Mellon University
15:30 - 16:50
Algorithmic VerificationPOPL at Turing Lecture
Chair(s): Andreas Pavlogiannis Aarhus University
15:30
20m
Talk
Polyregular functions on unordered trees of bounded height
POPL
Mikolaj Bojanczyk Warsaw University, Bartek Klin University of Oxford
15:50
20m
Talk
Solving Infinite-State Games via Acceleration
POPL
Philippe Heim CISPA Helmholtz Center for Information Security, Rayna Dimitrova CISPA Helmholtz Center for Information Security
Pre-print
16:10
20m
Talk
Ramsey Quantifiers in Linear Arithmetics
POPL
Pascal Bergsträßer University of Kaiserslautern-Landau, Moses Ganardi MPI-SWS, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Georg Zetzsche MPI-SWS
Pre-print
16:30
20m
Talk
Reachability in Continuous Pushdown VASS
POPL
A. R. Balasubramanian Technical University of Munich, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Uppsala University, Georg Zetzsche MPI-SWS
Pre-print
17:10 - 18:20
SIGPLAN Awards, PC Chair's Report, and Business MeetingPOPL at Kelvin Lecture
Chair(s): Philippa Gardner Imperial College London
17:10
70m
Awards
SIGPLAN Awards, PC Chair's Report, and Business Meeting
POPL

Fri 19 Jan

Displayed time zone: London change

08:50 - 09:00
WelcomePOPL at Kelvin Lecture +0min
08:50
10m
Other
Extraordinary Meeting: The Publicity Chairs Reflect on the Peer-Review Process
POPL
Alastair F. Donaldson Imperial College London, John Wickerson Imperial College London
08:50 - 09:00
WelcomePOPL at Turing Lecture
08:50
10m
Other
Extraordinary Meeting: The Publicity Chairs Reflect on the Peer-Review Process
POPL
Alastair F. Donaldson Imperial College London, John Wickerson Imperial College London
09:00 - 10:00
Keynote 2POPL at Kelvin Lecture
Chair(s): Alexandra Silva Cornell University
09:00
60m
Talk
The Network is the Computer: A Programming Language Perspective
POPL
Nate Foster Cornell University and Jane Street
10:30 - 11:50
Program AnalysisPOPL at Kelvin Lecture
Chair(s): Jules Villard Meta
10:30
20m
Talk
Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis
POPL
John Cyphert University of Wisconsin-Madison, USA, Zachary Kincaid Princeton University
10:50
20m
Talk
On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability
POPL
Shankaranarayanan Krishna IIT Bombay, India, Aniket Lal IIT Bombay, Andreas Pavlogiannis Aarhus University, Omkar Tuppe IIT Bombay
11:10
20m
Talk
Monotonicity and the Precision of Program Analysis
POPL
Marco Campion INRIA & École Normale Supérieure | Université PSL, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Arizona, Caterina Urban Inria & École Normale Supérieure | Université PSL
11:30
20m
Talk
Flan: An Expressive and Efficient Datalog Compiler for Program AnalysisDistinguished PaperRemote
POPL
Supun Abeysinghe Purdue University, Anxhelo Xhebraj Purdue University, Tiark Rompf Purdue University
10:30 - 11:50
Type TheoryPOPL at Turing Lecture
Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota
10:30
20m
Talk
Internal parametricity, without an interval
POPL
Thorsten Altenkirch University of Nottingham, Yorgo Chamoun École Polytechnique, Ambrus Kaposi Eötvös Loránd University, Michael Shulman University of San Diego
Pre-print
10:50
20m
Talk
Internal and Observational Parametricity for Cubical Agda
POPL
Antoine Van Muylder KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese KU Leuven
11:10
20m
Talk
Internalizing Indistinguishability with Dependent TypesRemote
POPL
Yiyun Liu University of Pennsylvania, Jonathan Chan University of Pennsylvania, Jessica Shi University of Pennsylvania, Stephanie Weirich University of Pennsylvania
11:30
20m
Talk
Polynomial Time and Dependent types
POPL
Robert Atkey University of Strathclyde
13:20 - 14:40
Types 3POPL at Kelvin Lecture
Chair(s): Steven Ramsay University of Bristol
13:20
20m
Talk
When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism
POPL
Lionel Parreaux HKUST (The Hong Kong University of Science and Technology), Aleksander Boruch-Gruszecki EPFL, Andong Fan HKUST (The Hong Kong University of Science and Technology), Chun Yin Chau HKUST (The Hong Kong University of Science and Technology)
DOI Pre-print File Attached
13:40
20m
Talk
Parametric Subtyping for Structural Parametric PolymorphismDistinguished PaperRemote
POPL
Henry DeYoung CMU, Andreia Mordido University of Lisbon, Frank Pfenning Carnegie Mellon University, USA, Ankush Das Amazon
14:00
20m
Talk
Unboxed data constructors -- or, how cpp decides a halting problem
POPL
Nicolas Chataing ENS Paris, Stephen Dolan Jane Street, Gabriel Scherer INRIA Saclay, Jeremy Yallop University of Cambridge
14:20
20m
Talk
Polymorphic Type Inference for Dynamic Languages
POPL
Giuseppe Castagna CNRS; Université Paris Cité, Mickaël Laurent Université Paris Cité / IRIF, Kim Nguyễn Université Paris-Saclay
Link to publication DOI
13:20 - 14:40
MedleyPOPL at Turing Lecture
Chair(s): Xiaokang Qiu Purdue University
13:20
20m
Talk
Guided Equality Saturation
POPL
Thomas Koehler INRIA, Andrés Goens University of Amsterdam, Siddharth Bhat the University of Edinburgh, Tobias Grosser University of Edinburgh, Phil Trinder University of Glasgow, Michel Steuwer TU Berlin; University of Edinburgh
Pre-print
13:40
20m
Talk
Fusing Direct Manipulations into Functional Programs
POPL
Xing Zhang Peking University, Ruifeng Xie Peking University, Guanchen Guo Peking University, Xiao He University of Science and Technology Beijing, Tao Zan Longyan University, Zhenjiang Hu Peking University
Pre-print
14:00
20m
Talk
Inference of Robust Reachability Constraints
POPL
Yanis Sellami CEA, List, Univ. Grenoble Alpes, Guillaume Girol CEA, List, Université Paris Saclay, Frédéric Recoules CEA, List, Damien Couroussé Univ Grenoble Alpes, CEA, List, Sébastien Bardin CEA LIST, University Paris-Saclay
14:20
20m
Talk
Nominal Recursors as Epi-RecursorsDistinguished Paper
POPL
Andrei Popescu University of Sheffield
15:10 - 16:30
Machine and Automata LearningPOPL at Kelvin Lecture
Chair(s): Steven Holtzen Northeastern University
15:10
20m
Talk
Efficient CHAD
POPL
Tom Smeding Utrecht University, Matthijs Vákár Utrecht University
15:30
20m
Talk
ReLU Hull Approximation
POPL
Zhongkui Ma The University of Queensland, Jiaying LI Microsoft, Guangdong Bai The University of Queensland
15:50
20m
Talk
On Learning Polynomial Recursive Programs
POPL
Alex Buna-Marginean University of Oxford, Vincent Cheval Inria Paris, Mahsa Shirmohammadi CNRS & IRIF, Paris, James Worrell University of Oxford
16:10
20m
Talk
Programming-by-Demonstration for Long-Horizon Robot Tasks
POPL
Noah Patton The University of Texas at Austin, Kia Rahmani The University of Texas at Austin, Meghana Missula The University of Texas at Austin, Joydeep Biswas The University of Texas at Austin, Işıl Dillig University of Texas at Austin
15:10 - 16:30
Mechanized ProofsPOPL at Turing Lecture
Chair(s): Andrei Popescu University of Sheffield
15:10
20m
Talk
Mechanizing Refinement Types
POPL
Michael Borkowski University of California, San Diego, Niki Vazou IMDEA Software Institute, Ranjit Jhala University of California at San Diego
15:30
20m
Talk
VST-A: A Foundationally Sound Annotation Verifier
POPL
Litao Zhou Shanghai Jiao Tong University; University of Hong Kong, Jianxing Qin Shanghai Jiao Tong University, Qinshi Wang Princeton University, Andrew W. Appel Princeton University, Qinxiang Cao Shanghai Jiao Tong University
15:50
20m
Talk
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
POPL
Ling Zhang Shanghai Jiao Tong University, Yuting Wang Shanghai Jiao Tong University, Jinhua Wu Shanghai Jiao Tong University, Jérémie Koenig Yale University, Zhong Shao Yale University
Pre-print
16:10
20m
Talk
A Formalization of Core Why3 in Coq
POPL
Joshua M. Cohen Princeton University, Philip Johnson-Freyd Sandia National Laboratories
16:50 - 18:10
Gradual Typing and VerificationPOPL at Kelvin Lecture
Chair(s): Ronald Garcia University of British Columbia
16:50
20m
Talk
Securing Verified IO Programs Against Unverified Code in F*
POPL
Cezar-Constantin Andrici MPI-SP, Stefan Ciobaca Alexandru Ioan Cuza University of Iasi, Cătălin Hriţcu MPI-SP, Guido Martínez Microsoft Research, Exequiel Rivas Tallinn University of Technology, Éric Tanter University of Chile, Theo Winterhalter INRIA Saclay
Pre-print
17:10
20m
Talk
Sound Gradual Verification with Symbolic Execution
POPL
Conrad Zimmerman Brown University, Jenna DiVincenzo (Wise) Purdue University, Jonathan Aldrich Carnegie Mellon University
17:30
20m
Talk
Type-based Gradual Typing Performance Optimization
POPL
John Peter Campora Quantinuum, Mohammad Wahiduzzaman Khan UL Lafayette, Sheng Chen UL Lafayette
17:50
20m
Talk
Total Type Error Localization and Recovery with HolesDistinguished Paper
POPL
Eric Zhao University of Michigan, Raef Maroof University of Michigan, Anand Dukkipati University of Michigan, Andrew Blinn University of Michigan, Zhiyi Pan University of Michigan, Cyrus Omar University of Michigan
16:50 - 17:50
Logical FoundationsPOPL at Turing Lecture
Chair(s): Emanuele D’Osualdo MPI-SWS
16:50
20m
Talk
Orthologic with Axioms
POPL
Simon Guilloud École Polytechnique Fédérale de Lausanne, Viktor Kunčak EPFL, Switzerland
Pre-print
17:10
20m
Talk
Deciding Asynchronous Hyperproperties for Recursive Programs
POPL
Jens Oliver Gutsfeld Westfälische Wilhelm-Universität Münster (WWU), Germany, Markus Müller-Olm University of Münster, Christoph Ohrem University of Münster
Pre-print
17:30
20m
Talk
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
POPL
Patrick Cousot New York University
18:10 - 18:15
Farewell from the ChairPOPL at Kelvin Lecture +0min
18:10 - 18:15
Farewell from the ChairPOPL at Turing Lecture

Accepted Papers

The proceedings of POPL 2024 are freely available as a special issue (Volume 8, No. POPL) of the PACMPL journal.

Title
A Case for Synthesis of Recursive Quantum Unitary Programs
POPL
A Core Calculus for Documents: Or, Lambda: The Ultimate Document
POPL
Pre-print
A Formalization of Core Why3 in Coq
POPL
Algebraic Effects Meet Hoare Logic in Cubical Agda
POPL
Pre-print
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
POPL
Pre-print
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive VerificationDistinguished Paper
POPL
Link to publication DOI
An Iris Instance for Verifying CompCert C Programs
POPL
Pre-print
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers
POPL
API-driven Program Synthesis for Testing Static Typing Implementations
POPL
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
POPL
DOI Pre-print
A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
POPL
Automatic Parallelism ManagementDistinguished Paper
POPL
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
POPL
Capturing Types (TOPLAS)
POPL
DOI File Attached
Coarser Equivalences for Causal Concurrency
POPL
Pre-print
Commutativity Simplifies Proofs of Parameterized Programs
POPL
Pre-print
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
POPL
Pre-print
Decalf: A Directed, Effectful Cost-Aware Logical Framework
POPL
Pre-print
Deciding Asynchronous Hyperproperties for Recursive Programs
POPL
Pre-print
Decision and Complexity of Dolev-Yao Hyperproperties
POPL
Disentanglement with Futures, State, and Interaction
POPL
DisLog: A Separation Logic for Disentanglement
POPL
Pre-print
EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
POPL
Effectful Software Contracts
POPL
Efficient Bottom-Up Synthesis for Programs with Local Variables
POPL
Pre-print
Efficient CHAD
POPL
Efficient Matching of Regular Expressions with Lookaround Assertions
POPL
Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations
POPL
Enriched Presheaf Model of Quantum FPC
POPL
Explicit Effects and Effect Constraints in ReML
POPL
Link to publication DOI
Flan: An Expressive and Efficient Datalog Compiler for Program AnalysisDistinguished PaperRemote
POPL
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
POPL
Pre-print
Fusing Direct Manipulations into Functional Programs
POPL
Pre-print
Generating Well-Typed Terms that are not "Useless"
POPL
Guided Equality Saturation
POPL
Pre-print
Higher Order Bayesian Networks, Exactly
POPL
How Hard is Weak-Memory Testing?
POPL
Pre-print
Ill-Typed Programs Don't Evaluate
POPL
Implementation and Synthesis of Math Library FunctionsDistinguished Paper
POPL
Indexed Types for a Statically Safe WebAssembly
POPL
DOI Pre-print
Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
POPL
Inference of Robust Reachability Constraints
POPL
Internal and Observational Parametricity for Cubical Agda
POPL
Internalizing Indistinguishability with Dependent TypesRemote
POPL
Internal parametricity, without an interval
POPL
Pre-print
Mechanizing Refinement Types
POPL
Modular Denotational Semantics for Effects with Guarded Interaction TreesDistinguished PaperRemote
POPL
DOI Pre-print
Monotonicity and the Precision of Program Analysis
POPL
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking FunctionsRemote
POPL
Nominal Recursors as Epi-RecursorsDistinguished Paper
POPL
On Learning Polynomial Recursive Programs
POPL
On Model-Checking Higher-Order Effectful Programs
POPL
On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability
POPL
Optimal Program Synthesis via Abstract Interpretation
POPL
Orthologic with Axioms
POPL
Pre-print
Parametric Subtyping for Structural Parametric PolymorphismDistinguished PaperRemote
POPL
Parikh's Theorem Made Symbolic
POPL
Pipelines and Beyond: Graph Types for ADTs with Futures
POPL
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic ProgramsRemote
POPL
Polymorphic Type Inference for Dynamic Languages
POPL
Link to publication DOI
Polynomial Time and Dependent types
POPL
Polyregular functions on unordered trees of bounded height
POPL
Positive Almost-Sure Termination – Complexity and Proof Rules
POPL
Predictive Monitoring against Pattern Regular Languages
POPL
Pre-print
Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
POPL
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
POPL
Programming-by-Demonstration for Long-Horizon Robot Tasks
POPL
Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-Deterministic Observers
POPL
Quotient Haskell: Lightweight Quotient Types for All
POPL
Ramsey Quantifiers in Linear Arithmetics
POPL
Pre-print
Reachability in Continuous Pushdown VASS
POPL
Pre-print
Regular Abstractions for Array Systems
POPL
ReLU Hull Approximation
POPL
Securing Verified IO Programs Against Unverified Code in F*
POPL
Pre-print
Semantic Code Refactoring for Abstract Data Types
POPL
Shoggoth - A Formal Foundation for Strategic Rewriting
POPL
Pre-print
SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog CompilationRemote
POPL
Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis
POPL
Solving Infinite-State Games via Acceleration
POPL
Pre-print
Sound Gradual Verification with Symbolic Execution
POPL
Soundly Handling LinearityDistinguished Paper
POPL
DOI Pre-print
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
POPL
The Complex(ity) Landscape of Checking Infinite Descent
POPL
The Essence of Generalized Algebraic Data TypesRemote
POPL
The Logical Essence of Well-Bracketed Control Flow
POPL
Thunks and Debits in Separation Logic with Time Credits
POPL
Total Type Error Localization and Recovery with HolesDistinguished Paper
POPL
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
POPL
Type-based Gradual Typing Performance Optimization
POPL
Unboxed data constructors -- or, how cpp decides a halting problem
POPL
Validation of Modern JSON Schema: Formalization and Complexity
POPL
DOI
VST-A: A Foundationally Sound Annotation Verifier
POPL
When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism
POPL
DOI Pre-print File Attached
With a Few Square Roots, Quantum Computing is as Easy as Pi
POPL
Pre-print

POPL 2024 Call for Papers

PACMPL Issue POPL 2024 seeks contributions on all aspects of programming languages and programming systems, both theoretical and practical. Authors of papers published in PACMPL Issue POPL 2024 will be invited to present their work in the POPL conference in January 2024, 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. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation, or application of programming languages.

Evaluation Criteria

The Program 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.

Full Double-Blind Reviewing Process

POPL 2024 will use a full double-blind reviewing process (similar to the one used for POPL 2023 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. Links to supplementary material on external websites are not permitted.

  • 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.

Additional Details of the Reviewing Process

POPL 2024 will have four Associate Chairs who will help the Program 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 but recommended. A response should address specific points or questions raised in the reviews as well as any erroneous claims made by reviewers; in particular, it should not present new technical results, unless specifically requested by the reviewers.

The Program Committee (PC) will discuss papers electronically using the HotCRP conference management system. There will be no physical or synchronous PC meeting; this will avoid the time, cost, and environmental impact of transporting an increasingly large committee to one point on the globe. There is also no formal External Program Committee or Extended Review Committee, though experts outside the committee will be consulted as needed. Paper decisions will be accompanied by a “meta-review” summarizing the reasoning behind the committee’s decision.

To conform with ACM requirements for journal publication, all POPL papers will be subject to two rounds of review. At the end of the first round, the PC will select a set of conditionally accepted papers, each with a clear list of mandatory revisions that the authors must implement in order for the paper to be accepted. For the second round, authors of conditionally accepted papers will then be required to submit a short description of how they have revised the paper, including how the mandatory revisions have been implemented. The PC will then check the revisions and make final acceptance decisions. Authors of conditionally accepted papers must submit a satisfactory revision to the PC by the second-round 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 2024, policies specified in this Call for Papers supersede those in the Principles of POPL document.

Submission Site Information

The submission site is https://popl24.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:59 PM on July 11, 2023, 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 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 ask 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.

  • We strongly encourage use of author-year citations, since that is the citation format required by PACMPL for final versions of accepted papers.

  • 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 will be given the opportunity to present their work at the conference in the form of a short talk. It is recommended that they give a talk in person at the conference, so that everyone can get the most out of the conference experience. However, authors 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. All presenting authors will be required to register for the conference. Authors also have the option of not presenting their work at the conference, in which case they do not need to register.

Distinguished Paper Awards

At most 10% of the accepted papers of POPL 2024 will be designated as Distinguished Papers. This award highlights papers that the Program 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. Please do not provide supplementary materials via links to external web sites. It is possible to change the linked items after the submission deadline has passed, and, to be fair to all authors, we would like to be sure reviewers evaluate materials that have been completed prior to the submission deadline.

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: Authors should not submit links to public repositories as supplementary material. In general, most code in a public repository can be repackaged and anonymized and submitted as a tarball at the time of paper submission. (Note: it is only necessary to anonymize new code that is part of the contribution of the paper, not pre-existing code or libraries on which one is building.)

However, there may be cases where this anonymization is for some reason difficult or impossible. In that case, authors should explain this in the “Confidential Comments for the Program Chair” field of their submission and include the link to a public repository there. The Program Chair and Associate Chairs will then decide (on a case-by-case basis) whether it is appropriate to share this link with reviewers. Needless to say, attempting to discover the reviewers for your paper by tracking visitors to a public repository would constitute a breach of academic integrity.

The same goes for online demos. A link to an online demo should only be given in the Confidential Comments for the Program Chair.

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: As explained above, authors should not do this. If you discover that they have done so, please bring it to the attention of the Program Chair.

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.