The annual Symposium on Principles of Programming Languages 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.

The symposium is sponsored by ACM SIGPLAN, in cooperation with ACM SIGACT and ACM SIGLOG.

The five-minute videos associated with the papers are now available on YouTube!

Dates

This program is tentative and subject to change.

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

Wed 19 Jan

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

08:00 - 09:00
BreakfastPOPL at Salon II
08:50 - 09:00
WelcomePOPL at Salon I
Chair(s): Rajeev Alur University of Pennsylvania, Hongseok Yang KAIST
09:00 - 10:00
Invited TalkPOPL at Salon I
Chair(s): Rajeev Alur University of Pennsylvania
09:00
60m
Keynote
Principles of Programming Language TranslatorsRemoteInvited Talk
POPL
Alfred V. Aho Columbia University
10:00 - 10:20
BreakPOPL at Salon II
10:20 - 12:00
Automated VerificationPOPL at Salon I
Chair(s): Roberto Giacobazzi University of Verona and IMDEA Software Institute
10:20
25m
Research paper
Software Model-Checking as Cyclic-Proof SearchRemote
POPL
Takeshi Tsukada Chiba University, Japan, Hiroshi Unno University of Tsukuba
10:45
25m
Research paper
Induction Duality: Primal-Dual Search for InvariantsRemote
POPL
Oded Padon VMware Research, James R. Wilcox University of Washington, Jason R. Koenig Stanford University, USA, Kenneth L. McMillan UT Austin, Alex Aiken Stanford University, USA
Pre-print
11:10
25m
Research paper
Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive FunctionsRemote
POPL
Hari Govind V K University of Waterloo, Sharon Shoham Tel Aviv University, Arie Gurfinkel University of Waterloo
11:35
25m
Research paper
Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And VariablesRemote
POPL
Taolue Chen University of London, Matthew Hague Royal Holloway, University of London, Zhilei Han School of Software, Tsinghua University, Denghang Hu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Alejandro Flores Lamas Royal Holloway University of London, Anthony Widjaja Lin Technische Universität Kaiserslautern and Max-Planck Institute for Software Systems, Shuanglong Kan Technische Universität Kaiserslautern, Philipp Ruemmer Uppsala University, Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
10:20 - 12:00
Separation LogicPOPL at Salon III
Chair(s): James Riely DePaul University
10:20
25m
Talk
A Separation Logic for Heap Space under Garbage CollectionRemote
POPL
10:45
25m
Research paper
Simuliris: A Separation Logic Framework for Verifying Concurrent Program OptimizationsDistinguished PaperRemote
POPL
Lennard Gäher MPI-SWS & Saarland University, Michael Sammler MPI-SWS, Simon Spies MPI-SWS, Ralf Jung MIT, Hoang-Hai Dang MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Jeehoon Kang KAIST, Derek Dreyer MPI-SWS
11:10
25m
Research paper
Concurrent Incorrectness Separation LogicRemote
POPL
Azalea Raad Imperial College London, Josh Berdine Facebook, Derek Dreyer MPI-SWS, Peter W. O'Hearn Facebook and University College London
11:35
25m
Research paper
On Incorrectness Logic and Kleene Algebra With Top and TestsInPerson
POPL
Cheng Zhang Boston University, Arthur Azevedo de Amorim Boston University, USA, Marco Gaboardi Boston University
12:00 - 13:30
LunchPOPL at Salon II
13:30 - 14:45
Program AnalysisPOPL at Salon I
Chair(s): Gagandeep Singh University of Illinois at Urbana-Champaign
13:30
25m
Research paper
Property-Directed Reachability as Abstract Interpretation in the Monotone TheoryRemote
POPL
Yotam M. Y. Feldman Tel Aviv University, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv University, James R. Wilcox University of Washington
13:55
25m
Research paper
Partial (In)Completeness in Abstract InterpretationInPerson
POPL
Marco Campion University of Verona, Mila Dalla Preda University of Verona, Italy, Roberto Giacobazzi University of Verona and IMDEA Software Institute
DOI Authorizer link Media Attached
14:20
25m
Research paper
Return of CFA: Call-Site Sensitivity Can Be Superior to Object Sensitivity Even for Object-Oriented ProgramsInPerson
POPL
Minseok Jeon Korea University, Hakjoo Oh Korea University
13:30 - 14:45
Weak Memory ModelsPOPL at Salon III
Chair(s): Mae Milano University of California, Berkeley
13:30
25m
Research paper
The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory ConcurrencyInPerson
POPL
Alan Jeffrey Roblox, James Riely DePaul University, Mark Batty University of Kent, Simon Cooksey University of Kent, Ilya Kaysin JetBrains Research; University of Cambridge, Anton Podkopaev HSE University; JetBrains Research
Pre-print
13:55
25m
Research paper
Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-Temporal StoresRemote
POPL
Azalea Raad Imperial College London, Luc Maranget Inria Paris, Viktor Vafeiadis MPI-SWS
14:20
25m
Research paper
Truly Stateless, Optimal Dynamic Partial Order ReductionRemote
POPL
Michalis Kokologiannakis MPI-SWS, Germany, Iason Marmanis MPI-SWS, Vladimir Gladstein MPI-SWS, JetBrains Research and St Petersburg University, Viktor Vafeiadis MPI-SWS
14:45 - 15:05
BreakPOPL at Salon II
15:05 - 16:20
Algorithmic Verification 1POPL at Salon I
Chair(s): Qirun Zhang Georgia Institute of Technology, USA
15:05
25m
Research paper
Efficient Algorithms for Dynamic Bidirected Dyck-ReachabilityRemote
POPL
Yuanbo Li Georgia Institute of Technology, USA, Kris Satya Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology, USA
15:30
25m
Research paper
The Decidability and Complexity of Interleaved Bidirected Dyck ReachabilityRemote
POPL
Adam Husted Kjelstrøm Aarhus University, Andreas Pavlogiannis Aarhus University
15:55
25m
Research paper
Subcubic Certificates for CFL ReachabilityRemote
POPL
Dmitry Chistikov University of Warwick, Rupak Majumdar MPI-SWS, Philipp Schepper CISPA
15:05 - 16:20
Concurrency and ParallelismPOPL at Salon III
Chair(s): Andrew C. Myers Cornell University
15:05
25m
Research paper
Visibility Reasoning for Concurrent Snapshot AlgorithmsRemote
POPL
Joakim Öhman IMDEA Software Institute, Aleksandar Nanevski IMDEA Software Institute
15:30
25m
Research paper
Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation LogicRemote
POPL
Jules Jacobs Radboud University Nijmegen, Stephanie Balzer Carnegie Mellon University, USA, Robbert Krebbers Radboud University Nijmegen
15:55
25m
Research paper
Static Prediction of Parallel Computation GraphsInPerson
POPL
Stefan K. Muller Illinois Institute of Technology
16:20 - 16:40
BreakPOPL at Salon II
16:40 - 17:30
Algorithmic Verification 2POPL at Salon I
Chair(s): Qirun Zhang Georgia Institute of Technology, USA
16:40
25m
Research paper
Context-Bounded Verification of Thread PoolsRemote
POPL
Pascal Baumann Max Planck Institute for Software Systems (MPI-SWS), Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Max Planck Institute for Software Systems (MPI-SWS), Georg Zetzsche Max Planck Institute for Software Systems (MPI-SWS)
17:05
25m
Research paper
What's Decidable about Linear Loops?InPerson
POPL
Toghrul Karimov Max Planck Institute for Software Systems, Engel Lefaucheux Max Planck Institute for Software Systems, Joël Ouaknine Max Planck Institute for Software Systems and University of Oxford, David Purser Max Planck Institute for Software Systems, Anton Varonka Max Planck Institute for Software Systems, Markus A. Whiteland Max Planck Institute for Software Systems, James Worrell University of Oxford
Pre-print
16:40 - 17:30
Reasoning about Probabilistic Programs and AlgorithmsPOPL at Salon III
Chair(s): Armando Solar-Lezama Massachusetts Institute of Technology
16:40
25m
Research paper
A Separation Logic for Negative DependenceRemote
POPL
Jialu Bao Cornell University, Marco Gaboardi Boston University, Justin Hsu University of Wisconsin-Madison, USA, Joseph Tassarotti Boston College
17:05
25m
Research paper
Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and RecursionRemote
POPL
Yizhou Zhang University of Waterloo, Nada Amin Harvard University
18:00 - 20:00
ReceptionPOPL at Salon II

Thu 20 Jan

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

08:00 - 09:00
BreakfastPOPL at Salon II
09:00 - 10:00
Invited TalkPOPL at Salon I
Chair(s): Michael Hicks University of Maryland at College Park
09:00
60m
Keynote
Better Learning through Programming LanguagesInvited TalkInPerson
POPL
Armando Solar-Lezama Massachusetts Institute of Technology
10:00 - 10:20
BreakPOPL at Salon II
10:20 - 12:00
Foundation and Verification of Machine-Learning SystemsPOPL at Salon I
Chair(s): Gilbert Louis Bernstein University of California at Berkeley, USA
10:20
25m
Research paper
A Dual Number Abstraction for Static Analysis of Clarke JacobiansInPerson
POPL
Jacob Laurel University of Illinois at Urbana-Champaign, Rem Yang University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign, Sasa Misailovic University of Illinois at Urbana-Champaign
10:45
25m
Research paper
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic DifferentiationRemote
POPL
Faustyna Krawiec University of Cambridge, Simon Peyton Jones Epic Games, Neel Krishnaswami Computer Laboratory, University of Cambridge, Tom Ellis Microsoft, Richard A. Eisenberg Tweag, Andrew Fitzgibbon Microsoft Research, Cambridge
11:10
25m
Research paper
Interval Universal Approximation for Neural NetworksInPerson
POPL
Zi Wang University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison, USA, Gautam Prakriya Chinese University of Hong Kong, Somesh Jha University of Wisconsin, Madison
11:35
25m
Research paper
PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull ApproximationsInPerson
POPL
Mark Niklas Müller ETH Zurich, Gleb Makarchuk ETH Zurich, Gagandeep Singh University of Illinois at Urbana-Champaign, Markus Püschel ETH Zurich, Switzerland, Martin Vechev ETH Zurich, Switzerland
10:20 - 12:00
Quantum ComputingPOPL at Salon III
Chair(s): Michael Hicks University of Maryland at College Park
10:20
25m
Research paper
Quantum Information EffectsRemote
POPL
Robin Kaarsgaard University of Edinburgh, Chris Heunen University of Edinburgh
10:45
25m
Research paper
Twist: Sound Reasoning for Purity and Entanglement in Quantum ProgramsInPerson
POPL
Charles Yuan Massachusetts Institute of Technology, Christopher McNally MIT, Michael Carbin Massachusetts Institute of Technology
11:10
25m
Research paper
Quantum Separation Logic: A Framework for Local Reasoning of Quantum ProgramsRemote
POPL
Xuan-Bach Le , Jun Sun Singapore Management University, Shang-Wei Lin Nanyang Technological University, Singapore, David Sanan Nanyang Technological University
11:35
25m
Research paper
Semantics for Variational Quantum ProgrammingRemote
POPL
Xiaodong Jia Hunan University, Andre Kornell Tulane University, Bert Lindenhovius Tulane University, Michael Mislove Tulane, Vladimir Zamdzhiev Inria
12:00 - 13:30
LunchPOPL at Salon II
13:30 - 14:45
TypesPOPL at Salon I
Chair(s): Stephanie Weirich University of Pennsylvania
13:30
25m
Research paper
On Type-Cases, Union Elimination, and Occurrence TypingInPerson
POPL
Giuseppe Castagna CNRS - Université de Paris, France, Mickaël Laurent Université de Paris, Kim Nguyễn University of Paris-Sud, France, Matthew Lutze Université de Paris
13:55
25m
Research paper
Oblivious Algebraic Data TypesInPerson
POPL
Qianchuan Ye Purdue University, Benjamin Delaware Purdue University
Pre-print
14:20
25m
Research paper
SolType: Refinement Types for SolidityRemote
POPL
Bryan Tan University of California, Santa Barbara, Benjamin Mariano University of Texas at Austin, Shuvendu Lahiri Microsoft, Isil Dillig University of Texas at Austin, Yu Feng University of California at Santa Barbara
13:30 - 14:45
Dynamic AnalysisPOPL at Salon III
Chair(s): Armando Solar-Lezama Massachusetts Institute of Technology
13:30
25m
Research paper
A formal foundation for symbolic evaluation with mergingRemote
POPL
Sorawee Porncharoenwase University of Washington, Luke Nelson University of Washington, Xi Wang University of Washington, Emina Torlak University of Washington
13:55
25m
Research paper
Logarithm and Program TestingInPerson
POPL
Kuen-Bang Hou (Favonia) University of Minnesota, Twin Cities, Zhuyang Wang University of Minnesota
DOI Media Attached
14:20
25m
Research paper
Profile Inference RevisitedRemote
POPL
Wenlei He Facebook, Juli\'{a}n Mestre Facebook, Sergey Pupyrev Facebook, Lei Wang Facebook, Hongtao Yu Facebook
14:45 - 15:05
BreakPOPL at Salon II
15:05 - 16:20
SystemsPOPL at Salon I
Chair(s): Arthur Azevedo de Amorim Boston University, USA
15:05
25m
Research paper
Isolation Without Taxation: Near Zero Cost Transitions for WebAssembly and SFIInPerson
POPL
Matthew Kolosick University of California, San Diego, Shravan Ravi Narayan University of California, San Diego, Evan Johnson University of California, San Diego, Conrad Watt University of Cambridge, UK, Michael LeMay Intel Labs, Deepak Garg MPI-SWS, Ranjit Jhala University of California at San Diego, Deian Stefan University of California at San Diego, USA
15:30
25m
Research paper
Relational E-MatchingRemote
POPL
Yihong Zhang University of Washington, Yisu Remy Wang University of Washington, Max Willsey University of Washington, Zachary Tatlock University of Washington
Pre-print
15:55
25m
Research paper
Linked visualisations via Galois dependenciesRemote
POPL
Roly Perera The Alan Turing Institute/University of Bristol, Minh Nguyen University of Bristol, Tomas Petricek University of Kent, Meng Wang University of Bristol
Pre-print
15:05 - 16:20
MetaprogrammingPOPL at Salon III
Chair(s): Stephanie Weirich University of Pennsylvania
15:05
25m
Research paper
Staging with ClassInPerson
POPL
Ningning Xie University of Cambridge, Matthew Pickering University of Bristol, UK, Andres Löh Well-Typed LLP, Nicolas Wu Imperial College London, UK, Jeremy Yallop University of Cambridge, Meng Wang University of Bristol
Pre-print
15:30
25m
Research paper
Moebius: Metaprogramming using Contextual TypesRemote
POPL
Junyoung Jang McGill University, Samuel Gélineau SimSpace, Stefan Monnier Université de Montréal, Brigitte Pientka McGill University
15:55
25m
Research paper
Type-Level Programming with Match TypesRemote
POPL
Olivier Blanvillain EPFL, Jonathan Immanuel Brachthäuser University of Tübingen, Germany, Maxime Kjaer EPFL, Martin Odersky EPFL
16:20 - 16:40
BreakPOPL at Salon II
16:40 - 18:00
POPL Business Meeting and SIGPLAN AwardsPOPL at Salon I
Chair(s): Rajeev Alur University of Pennsylvania
16:40
10m
Meeting
General Chair ReportInPerson
POPL
Rajeev Alur University of Pennsylvania
16:50
10m
Meeting
Program Chair ReportRemote
POPL
17:00
10m
Meeting
Virtualization Chair ReportRemote
POPL
Adam Chlipala Massachusetts Institute of Technology
17:10
5m
Meeting
POPL 2023 ReportInPerson
POPL
Andrew C. Myers Cornell University
17:15
3m
Awards
Student Research Competition WinnersRemote
POPL
Azalea Raad Imperial College London
17:18
3m
Awards
POPL'22 Distinguished PapersRemote
POPL
17:21
3m
Awards
SIGPLAN Reynolds Dissertation AwardRemote
POPL
Isil Dillig University of Texas at Austin
17:24
3m
Awards
POPL Most Influential Paper AwardRemote
POPL
Tony Hosking Australian National University
17:27
3m
Awards
SIGPLAN Programming Languages Achievements AwardRemote
POPL
Isil Dillig University of Texas at Austin
17:30
10m
Awards
Remarks by SIGPLAN PL Achievements Award WinnerRemote
POPL

17:40
20m
Meeting
Open Forum for Q&AInPerson
POPL
Rajeev Alur University of Pennsylvania

Fri 21 Jan

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

08:00 - 09:00
BreakfastPOPL at Salon II
09:00 - 10:00
Invited TalkPOPL at Salon I
Chair(s): Adam Chlipala Massachusetts Institute of Technology
09:00
60m
Keynote
Coalgebra for the working programming languages researcherRemoteInvited Talk
POPL
Alexandra Silva Cornell University
10:00 - 10:20
BreakPOPL at Salon II
10:20 - 12:00
Distributed or Network ProgramsPOPL at Salon I
Chair(s): J. Garrett Morris The University of Iowa
10:20
25m
Research paper
Pirouette: Higher-Order Typed Functional ChoreographiesDistinguished PaperInPerson
POPL
Andrew K. Hirsch Max Planck Institute for Software Systems, Deepak Garg MPI-SWS
Pre-print
10:45
25m
Research paper
Fair termination of binary sessionsRemote
POPL
Luca Ciccone Università di Torino, Italy, Luca Padovani University of Turin, Italy
11:10
25m
Research paper
Safe, Modular Packet Pipeline ProgrammingRemote
POPL
Devon Loehr Princeton University, USA, David Walker Princeton University, USA
11:35
25m
Research paper
Dependently-Typed Data Plane ProgrammingRemote
POPL
Matthias Eichholz TU Darmstadt, Germany, Eric Campbell Cornell University, Matthias Krebs TU Darmstadt, Germany, Nate Foster Cornell University, Mira Mezini TU Darmstadt, Germany
10:20 - 12:00
Semantics 1POPL at Salon III
Chair(s): Alan Jeffrey Roblox
10:20
25m
Research paper
From Enhanced Coinduction towards Enhanced InductionRemote
POPL
Davide Sangiorgi University of Bologna
10:45
25m
Research paper
A Fine-Grained Computational Interpretation of Girard's Intuitionistic Proof-NetsInPerson
POPL
Delia Kesner IRIF, France / University of Paris Diderot, France
11:10
25m
Research paper
Fully abstract models for effectful λ-calculi via category-theoretic logical relationsRemote
POPL
Philip Saville University of Oxford, Ohad Kammar University of Edinburgh, Shin-ya Katsumata National Institute of Informatics
11:35
25m
Research paper
Layered and Object-Based Game SemanticsInPerson
POPL
Arthur Oliveira Vale Yale University, Paul-André Melliès CNRS - Université de Paris, France, Zhong Shao Yale University, Jérémie Koenig Yale University, Leo Stefanesco IRIF, University Paris Diderot & CNRS
12:00 - 13:30
LunchPOPL at Salon II
13:30 - 14:45
TOPLAS SessionPOPL at Salon I
Chair(s): Andrew C. Myers Cornell University
13:30
25m
Talk
Armed cats: formal concurrency modelling at ArmRemote
POPL
Jade Alglave University College London, Will Deacon ARM Ltd., Richard Grisenthwaite , Antoine Hacquard EPITA, LRDE, Luc Maranget Inria Paris
13:55
25m
Talk
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs Remote
POPL
Emanuele D'Osualdo MPI-SWS, Julian Sutherland Imperial College London, Azadeh Farzan University of Toronto, Philippa Gardner Imperial College London
DOI
14:20
25m
Talk
Gradualizing the Calculus of Inductive ConstructionsRemote
POPL
Meven Lennon-Bertrand Inria – LS2N, Université de Nantes, Kenji Maillard Inria Nantes & University of Chile, Nicolas Tabareau Inria, Éric Tanter University of Chile
13:30 - 14:45
Semantics 2POPL at Salon III
Chair(s): Marco Gaboardi Boston University
13:30
25m
Research paper
Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming LanguagesInPerson
POPL
Vikraman Choudhury Indiana University & University of Cambridge, Jacek Karwowski University of Warsaw, Amr Sabry Indiana University
Link to publication DOI Pre-print
13:55
25m
Research paper
A Relational Theory of Effects and CoeffectsRemote
POPL
Ugo Dal Lago University of Bologna, Francesco Gavazzo University of Bologna & INRIA Sophia Antipolis
14:20
25m
Research paper
Effectful Program DistancingRemote
POPL
Ugo Dal Lago University of Bologna, Francesco Gavazzo University of Bologna & INRIA Sophia Antipolis
14:45 - 15:05
BreakPOPL at Salon II
15:05 - 16:20
Verification 1POPL at Salon I
Chair(s): Lennart Beringer Princeton University
15:05
25m
Research paper
Certifying Derivation of State Machines from CoroutinesInPerson
POPL
Mirai Ikebuchi National Institute of Informatics, Japan, Andres Erbsen MIT, Adam Chlipala Massachusetts Institute of Technology
15:30
25m
Research paper
VIP: Verifying Real-World C Idioms with Integer-Pointer CastsRemote
POPL
Rodolphe Lepigre MPI-SWS, Michael Sammler MPI-SWS, Kayvan Memarian University of Cambridge, Robbert Krebbers Radboud University Nijmegen, Derek Dreyer MPI-SWS, Peter Sewell University of Cambridge
15:55
25m
Research paper
Verified Compilation of C Programs with a Nominal Memory ModelRemote
POPL
Yuting Wang John Hopcroft Center for Computer Science - Shanghai Jiao Tong University, Ling Zhang John Hopcroft Center for Computer Science - Shanghai Jiao Tong University, Zhong Shao Yale University, Jérémie Koenig Yale University
15:05 - 16:20
Type TheoryPOPL at Salon III
Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota, Twin Cities
15:05
25m
Research paper
A cost-aware logical frameworkInPerson
POPL
Yue Niu Carnegie Mellon University, Jonathan Sterling Aarhus University, Denmark, Harrison Grodin Carnegie Mellon University, Robert Harper Carnegie Mellon University, USA
Pre-print Media Attached
15:30
25m
Research paper
Formal Metatheory of Second-Order Abstract SyntaxDistinguished PaperRemote
POPL
Marcelo Fiore Computer Laboratory, University of Cambridge, Dmitrij Szamozvancev University of Cambridge
15:55
25m
Research paper
Observational Equality: Now For GoodDistinguished PaperRemote
POPL
Loïc Pujet Gallinette Project-Team, Inria, Nicolas Tabareau Inria
16:20 - 16:40
BreakPOPL at Salon II
16:40 - 17:30
Verification 2POPL at Salon I
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
16:40
25m
Research paper
Verified Tensor-Program Optimization Via High-level Scheduling RewritesRemote
POPL
Amanda Liu Massachusetts Institute of Technology, Gilbert Louis Bernstein University of California at Berkeley, USA, Adam Chlipala Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology
17:05
25m
Research paper
One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding ModesDistinguished PaperRemote
POPL
Jay P. Lim Rutgers University, USA, Santosh Nagarakatte Rutgers University
Pre-print
16:40 - 17:30
SynthesisPOPL at Salon III
Chair(s): Paul Downen University of Massachusetts Lowell
16:40
25m
Research paper
Learning Formulas in Finite Variable LogicsDistinguished PaperInPerson
POPL
Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign
17:05
25m
Research paper
Bottom-up Synthesis of Recursive Functional Programs using Angelic ExecutionDistinguished PaperRemote
POPL
Anders Miltner The University of Texas at Austin, Texas, USA, Adrian Trejo Nuñez The University of Texas at Austin, Ana Brendel UT Austin, Swarat Chaudhuri UT Austin, Isil Dillig University of Texas at Austin
Hide past events

POPL 2022 Call for Papers

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

Scope

Principles of Programming Languages 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.

Evaluation Process

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 review; in particular, it must not introduce new technical results. Reviewers will write a short reaction to these author responses. The Review Committee will discuss papers entirely electronically rather than at a physical meeting. This will avoid the time, cost, and environmental impact of transporting an increasingly large committee to one point on the globe. There is no formal External Review Committee, though experts outside the committee will be consulted. 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.

For additional information about the reviewing process, see:

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.

Submission Guidelines

The following two points are easy to overlook:

  • Conflicts: Each author of a submission has to log into the submission system and properly declare all potential conflicts of interest in the author profile form. A conflict caught late in the reviewing process leads to a voided review which may be infeasible to replace.
  • Anonymity: POPL 2022 will employ a lightweight double-blind reviewing process. Make sure that your submitted paper is fully anonymized.

Prior to the paper submission deadline, the authors will upload their full anonymized paper. Each paper should have no more than 25 pages of text, excluding bibliography, using the new ACM Proceedings format. This format is chosen for compatibility with PACMPL. 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. PACMPL templates for Microsoft Word and LaTeX can be found at the SIGPLAN author information page. In particular, authors using LaTeX should use the acmart-pacmpl-template.tex file (with the acmsmall option). 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. Papers that exceed the length requirement, that deviate from the expected format, or that are submitted late will be rejected.

Deadlines expire at the end of the day, anywhere on earth on the Important Dates displayed to the right. Submitted papers must adhere to the SIGPLAN Republication Policy and the ACM Policy on Plagiarism. Concurrent submissions to other conferences, workshops, journals, or similar forums of publication are not allowed.

POPL 2022 will employ a lightweight double-blind reviewing process. To facilitate this, submitted papers must adhere to two rules:

  1. author names and institutions must be omitted, and
  2. references to authors’ own related work should be in the third person (e.g., not “We build on our previous work …” but rather “We build on the work of …”).

The purpose of this process is to help the Review Committee and external reviewers come to an initial judgment about the paper without bias, not to make it impossible for them to discover the authors if they were to try. Nothing should be done in the name of anonymity that weakens the submission or makes the job of reviewing the paper more difficult. In particular, important background references should not be omitted or anonymized. In addition, authors are free to disseminate their ideas or draft versions of their paper as usual. For example, authors may post drafts of their papers on the web or give talks on their research ideas. A document answering frequently asked questions addresses many common concerns.

The submission itself is the object of review and so it should strive to convince the reader of at least the plausibility of reported results. Still, we encourage authors to provide any supplementary material that is required to support the claims made in the paper, such as detailed proofs, proof scripts, or experimental data. These materials must be uploaded at submission time, as a single pdf or a tarball, not via a URL. Two forms of supplementary material may be submitted.

  1. Anonymous supplementary material is available to the reviewers before they submit their first-draft reviews.
  2. Non-anonymous supplementary material is available to the reviewers after they have submitted their first-draft reviews and learned the identity of the authors.

Use the anonymous form if possible. Reviewers are under no obligation to look at the supplementary material but may refer to it if they have questions about the material in the body of the paper.

Artifact Evaluation

Authors of 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. This submission is voluntary and will not influence the final decision regarding the papers. Papers that go through the Artifact Evaluation process successfully will receive a seal of approval printed on the papers themselves. Authors of accepted papers are encouraged to make these materials publicly available upon publication of the proceedings, by including them as “source materials” in the ACM Digital Library.

Copyright, Publication, and Presentation

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

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

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

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

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

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

Distinguished Paper Awards

At most 10% of the accepted papers of POPL 2022 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 a second review process.

Accepted Papers

Title
A cost-aware logical frameworkInPerson
POPL
Pre-print Media Attached
A Dual Number Abstraction for Static Analysis of Clarke JacobiansInPerson
POPL
A Fine-Grained Computational Interpretation of Girard's Intuitionistic Proof-NetsInPerson
POPL
A formal foundation for symbolic evaluation with mergingRemote
POPL
A Relational Theory of Effects and CoeffectsRemote
POPL
A Separation Logic for Heap Space under Garbage CollectionRemote
POPL
A Separation Logic for Negative DependenceRemote
POPL
Bottom-up Synthesis of Recursive Functional Programs using Angelic ExecutionDistinguished PaperRemote
POPL
Certifying Derivation of State Machines from CoroutinesInPerson
POPL
Concurrent Incorrectness Separation LogicRemote
POPL
Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation LogicRemote
POPL
Context-Bounded Verification of Thread PoolsRemote
POPL
Dependently-Typed Data Plane ProgrammingRemote
POPL
Effectful Program DistancingRemote
POPL
Efficient Algorithms for Dynamic Bidirected Dyck-ReachabilityRemote
POPL
Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-Temporal StoresRemote
POPL
Fair termination of binary sessionsRemote
POPL
Formal Metatheory of Second-Order Abstract SyntaxDistinguished PaperRemote
POPL
From Enhanced Coinduction towards Enhanced InductionRemote
POPL
Fully abstract models for effectful λ-calculi via category-theoretic logical relationsRemote
POPL
Induction Duality: Primal-Dual Search for InvariantsRemote
POPL
Pre-print
Interval Universal Approximation for Neural NetworksInPerson
POPL
Isolation Without Taxation: Near Zero Cost Transitions for WebAssembly and SFIInPerson
POPL
Layered and Object-Based Game SemanticsInPerson
POPL
Learning Formulas in Finite Variable LogicsDistinguished PaperInPerson
POPL
Linked visualisations via Galois dependenciesRemote
POPL
Pre-print
Logarithm and Program TestingInPerson
POPL
DOI Media Attached
Moebius: Metaprogramming using Contextual TypesRemote
POPL
Oblivious Algebraic Data TypesInPerson
POPL
Pre-print
Observational Equality: Now For GoodDistinguished PaperRemote
POPL
One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding ModesDistinguished PaperRemote
POPL
Pre-print
On Incorrectness Logic and Kleene Algebra With Top and TestsInPerson
POPL
On Type-Cases, Union Elimination, and Occurrence TypingInPerson
POPL
Partial (In)Completeness in Abstract InterpretationInPerson
POPL
DOI Authorizer link Media Attached
Pirouette: Higher-Order Typed Functional ChoreographiesDistinguished PaperInPerson
POPL
Pre-print
PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull ApproximationsInPerson
POPL
Profile Inference RevisitedRemote
POPL
Property-Directed Reachability as Abstract Interpretation in the Monotone TheoryRemote
POPL
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic DifferentiationRemote
POPL
Quantum Information EffectsRemote
POPL
Quantum Separation Logic: A Framework for Local Reasoning of Quantum ProgramsRemote
POPL
Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and RecursionRemote
POPL
Relational E-MatchingRemote
POPL
Pre-print
Return of CFA: Call-Site Sensitivity Can Be Superior to Object Sensitivity Even for Object-Oriented ProgramsInPerson
POPL
Safe, Modular Packet Pipeline ProgrammingRemote
POPL
Semantics for Variational Quantum ProgrammingRemote
POPL
Simuliris: A Separation Logic Framework for Verifying Concurrent Program OptimizationsDistinguished PaperRemote
POPL
Software Model-Checking as Cyclic-Proof SearchRemote
POPL
SolType: Refinement Types for SolidityRemote
POPL
Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive FunctionsRemote
POPL
Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And VariablesRemote
POPL
Staging with ClassInPerson
POPL
Pre-print
Static Prediction of Parallel Computation GraphsInPerson
POPL
Student Research Competition WinnersRemote
POPL
Subcubic Certificates for CFL ReachabilityRemote
POPL
Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming LanguagesInPerson
POPL
Link to publication DOI Pre-print
The Decidability and Complexity of Interleaved Bidirected Dyck ReachabilityRemote
POPL
The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory ConcurrencyInPerson
POPL
Pre-print
Truly Stateless, Optimal Dynamic Partial Order ReductionRemote
POPL
Twist: Sound Reasoning for Purity and Entanglement in Quantum ProgramsInPerson
POPL
Type-Level Programming with Match TypesRemote
POPL
Verified Compilation of C Programs with a Nominal Memory ModelRemote
POPL
Verified Tensor-Program Optimization Via High-level Scheduling RewritesRemote
POPL
VIP: Verifying Real-World C Idioms with Integer-Pointer CastsRemote
POPL
Visibility Reasoning for Concurrent Snapshot AlgorithmsRemote
POPL
What's Decidable about Linear Loops?InPerson
POPL
Pre-print