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 SIGPLAN YouTube channel now inclues the five-minute videos associated with the papers and the longer talk recordings from the conference!

Dates
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
10:20
25m
Research paper
Software Model-Checking as Cyclic-Proof SearchRemote
POPL
Takeshi Tsukada Chiba University, Hiroshi Unno University of Tsukuba; RIKEN AIP
DOI Media Attached
10:45
25m
Research paper
Induction Duality: Primal-Dual Search for InvariantsRemote
POPL
Oded Padon VMware Research; Stanford University, James R. Wilcox Certora, Jason R. Koenig Stanford University, Kenneth L. McMillan University of Texas at Austin, Alex Aiken Stanford University
DOI Media Attached
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
DOI Media Attached
11:35
25m
Research paper
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and VariablesRemote
POPL
Taolue Chen Birkbeck University of London, Alejandro Flores Lamas Royal Holloway University of London, Matthew Hague Royal Holloway University of London, Zhilei Han Tsinghua University, Denghang Hu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Shuanglong Kan TU Kaiserslautern, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer Uppsala University, Zhilin Wu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
DOI Media Attached
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; VMware
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 Certora
DOI Media Attached
13:55
25m
Research paper
Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program AnalysisInPerson
POPL
Marco Campion University of Verona, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Verona
DOI 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
DOI Media Attached
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
DOI Media Attached
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, Viktor Vafeiadis MPI-SWS
DOI Media Attached
14:20
25m
Research paper
Truly Stateless, Optimal Dynamic Partial Order ReductionRemote
POPL
Michalis Kokologiannakis MPI-SWS, Iason Marmanis MPI-SWS, Vladimir Gladstein MPI-SWS; St. Petersburg University; JetBrains Research, Viktor Vafeiadis MPI-SWS
DOI Media Attached
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
15:05
25m
Research paper
Efficient Algorithms for Dynamic Bidirected Dyck-ReachabilityRemote
POPL
Yuanbo Li Georgia Institute of Technology, Kris Satya Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology
DOI Media Attached
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
DOI Media Attached
15:55
25m
Research paper
Subcubic Certificates for CFL ReachabilityRemote
POPL
Dmitry Chistikov University of Warwick, Rupak Majumdar MPI-SWS, Philipp Schepper CISPA
DOI Media Attached
15:05 - 16:20
Concurrency and ParallelismPOPL at Salon III
Chair(s): Andrew Myers Cornell University
15:05
25m
Research paper
Visibility Reasoning for Concurrent Snapshot AlgorithmsRemote
POPL
Joakim Öhman IMDEA Software Institute; Universidad Politécnica de Madrid, Aleksandar Nanevski IMDEA Software Institute
DOI Media Attached
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, Robbert Krebbers Radboud University Nijmegen
DOI Media Attached
15:55
25m
Research paper
Static Prediction of Parallel Computation GraphsInPerson
POPL
Stefan K. Muller Illinois Institute of Technology
DOI Media Attached
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
16:40
25m
Research paper
Context-Bounded Verification of Thread PoolsRemote
POPL
DOI Media Attached
17:05
25m
Research paper
What’s Decidable about Linear Loops?InPerson
POPL
Toghrul Karimov MPI-SWS, Engel Lefaucheux MPI-SWS, Joël Ouaknine MPI-SWS, David Purser MPI-SWS, Anton Varonka MPI-SWS, Markus A. Whiteland MPI-SWS, James Worrell University of Oxford
DOI Pre-print Media Attached
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 Cornell University, Joseph Tassarotti Boston College
DOI Media Attached
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
DOI Media Attached
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 Bernstein University of California at Berkeley
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; VMware, Sasa Misailovic University of Illinois at Urbana-Champaign
DOI Media Attached
10:45
25m
Research paper
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic DifferentiationRemote
POPL
Faustyna Krawiec University of Cambridge, Simon Peyton Jones Microsoft Research, Neel Krishnaswami University of Cambridge, Tom Ellis Microsoft Research, Richard A. Eisenberg Tweag, Andrew Fitzgibbon Graphcore
DOI Media Attached
11:10
25m
Research paper
Interval Universal Approximation for Neural NetworksInPerson
POPL
Zi Wang University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison, Gautam Prakriya Chinese University of Hong Kong, Somesh Jha University of Wisconsin
DOI Media Attached
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; VMware, Markus Püschel ETH Zurich, Martin Vechev ETH Zurich
DOI Media Attached
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
Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Edinburgh
DOI Media Attached
10:45
25m
Research paper
Twist: Sound Reasoning for Purity and Entanglement in Quantum ProgramsInPerson
POPL
Charles Yuan Massachusetts Institute of Technology, Christopher McNally Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
DOI Media Attached
11:10
25m
Research paper
A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation LogicRemote
POPL
Xuan-Bach Le Nanyang Technological University, Shang-Wei Lin Nanyang Technological University, Jun Sun Singapore Management University, David Sanan Nanyang Technological University
DOI Media Attached
11:35
25m
Research paper
Semantics for Variational Quantum ProgrammingRemote
POPL
Xiaodong Jia Hunan University, Andre Kornell Tulane University, Bert Lindenhovius JKU Linz, Michael Mislove Tulane University, Vladimir Zamdzhiev Inria
DOI Media Attached
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, Mickaël Laurent Université de Paris, Kim Nguyễn Université Paris-Saclay, Matthew Lutze Université de Paris
DOI Media Attached
13:55
25m
Research paper
Oblivious Algebraic Data TypesInPerson
POPL
Qianchuan Ye Purdue University, Benjamin Delaware Purdue University
DOI Media Attached
14:20
25m
Research paper
SolType: Refinement Types for Arithmetic Overflow in SolidityRemote
POPL
Bryan Tan University of California at Santa Barbara, Benjamin Mariano University of Texas at Austin, Shuvendu K. Lahiri Microsoft Research, Işıl Dillig University of Texas at Austin, Yu Feng University of California at Santa Barbara
DOI Media Attached
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
DOI Media Attached
13:55
25m
Research paper
Logarithm and Program TestingInPerson
POPL
Kuen-Bang Hou (Favonia) University of Minnesota, Zhuyang Wang University of Minnesota
DOI Media Attached
14:20
25m
Research paper
Profile Inference RevisitedRemote
POPL
Wenlei He Facebook, Julián Mestre Facebook; University of Sydney, Sergey Pupyrev , Lei Wang Facebook, Hongtao Yu Facebook
DOI Media Attached
14:45 - 15:05
BreakPOPL at Salon II
15:05 - 16:20
SystemsPOPL at Salon I
Chair(s): Arthur Azevedo de Amorim Boston University
15:05
25m
Research paper
Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFIInPerson
POPL
Matthew Kolosick University of California at San Diego, Shravan Ravi Narayan University of California at San Diego, Evan Johnson University of California at San Diego, Conrad Watt University of Cambridge, Michael LeMay Intel Labs, Deepak Garg MPI-SWS, Ranjit Jhala University of California at San Diego, Deian Stefan University of California at San Diego
DOI Media Attached
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
DOI Media Attached
15:55
25m
Research paper
Linked Visualisations via Galois DependenciesRemote
POPL
Roly Perera Alan Turing Institute, Minh Nguyen University of Bristol, Tomas Petricek University of Kent, Meng Wang University of Bristol
DOI Media Attached
15:05 - 16:20
MetaprogrammingPOPL at Salon III
Chair(s): Stephanie Weirich University of Pennsylvania
15:05
25m
Research paper
Staging with Class: A Specification for Typed Template HaskellInPerson
POPL
Ningning Xie University of Toronto, Matthew Pickering Well-Typed LLP, Andres Löh Well-Typed LLP, Nicolas Wu Imperial College London, Jeremy Yallop University of Cambridge, Meng Wang University of Bristol
DOI Media Attached
15:30
25m
Research paper
Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on ItselfRemote
POPL
Junyoung Jang McGill University, Samuel Gélineau SimSpace, Stefan Monnier Université de Montréal, Brigitte Pientka McGill University
DOI Media Attached
15:55
25m
Research paper
Type-Level Programming with Match TypesRemote
POPL
DOI Media Attached
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 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
Işıl 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
Işıl 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 MPI-SWS, Deepak Garg MPI-SWS
DOI Media Attached
10:45
25m
Research paper
Fair Termination of Binary SessionsRemote
POPL
Luca Ciccone University of Turin, Luca Padovani University of Turin
DOI Media Attached
11:10
25m
Research paper
Safe, Modular Packet Pipeline ProgrammingRemote
POPL
Devon Loehr Princeton University, David Walker Princeton University
DOI Media Attached
11:35
25m
Research paper
Dependently-Typed Data Plane ProgrammingRemote
POPL
Matthias Eichholz TU Darmstadt, Eric Campbell Cornell University, Matthias Krebs TU Darmstadt, Nate Foster Cornell University, Mira Mezini TU Darmstadt
DOI Media Attached
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; Inria
DOI Media Attached
10:45
25m
Research paper
A Fine-Grained Computational Interpretation of Girard’s Intuitionistic Proof-NetsInPerson
POPL
Delia Kesner Université de Paris; CNRS; IRIF; Institut Universitaire de France
DOI Media Attached
11:10
25m
Research paper
Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical RelationsRemote
POPL
Ohad Kammar University of Edinburgh, Shin-ya Katsumata National Institute of Informatics, Philip Saville University of Oxford
DOI Media Attached
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, Zhong Shao Yale University, Jérémie Koenig Yale University, Leo Stefanesco IRIF, University Paris Diderot & CNRS
DOI Media Attached
12:00 - 13:30
LunchPOPL at Salon II
13:30 - 14:45
TOPLAS SessionPOPL at Salon I
Chair(s): Andrew 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
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 Media Attached
13:55
25m
Research paper
A Relational Theory of Effects and CoeffectsRemote
POPL
Ugo Dal Lago University of Bologna; Inria, Francesco Gavazzo University of Bologna; Inria
DOI Media Attached
14:20
25m
Research paper
Effectful Program DistancingRemote
POPL
Ugo Dal Lago University of Bologna; Inria, Francesco Gavazzo University of Bologna; Inria
DOI Media Attached
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, Andres Erbsen Massachusetts Institute of Technology, Adam Chlipala Massachusetts Institute of Technology
DOI Media Attached
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
DOI Media Attached
15:55
25m
Research paper
Verified Compilation of C Programs with a Nominal Memory ModelRemote
POPL
Yuting Wang Shanghai Jiao Tong University, Ling Zhang Shanghai Jiao Tong University, Zhong Shao Yale University, Jérémie Koenig Yale University
DOI Media Attached
15:05 - 16:20
Type TheoryPOPL at Salon III
Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota
15:05
25m
Research paper
A Cost-Aware Logical FrameworkInPerson
POPL
Yue Niu Carnegie Mellon University, Jonathan Sterling Aarhus University, Harrison Grodin Carnegie Mellon University, Robert Harper Carnegie Mellon University
DOI Media Attached
15:30
25m
Research paper
Formal Metatheory of Second-Order Abstract SyntaxDistinguished PaperRemote
POPL
Marcelo Fiore University of Cambridge, Dmitrij Szamozvancev University of Cambridge
DOI Media Attached
15:55
25m
Research paper
Observational Equality: Now for GoodDistinguished PaperRemote
POPL
DOI Media Attached
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 Bernstein University of California at Berkeley, Adam Chlipala Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology
DOI Media Attached
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, Santosh Nagarakatte Rutgers University
DOI Media Attached
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
DOI Media Attached
17:05
25m
Research paper
Bottom-Up Synthesis of Recursive Functional Programs using Angelic ExecutionDistinguished PaperRemote
POPL
Anders Miltner University of Texas at Austin, Adrian Trejo Nuñez University of Texas at Austin, Ana Brendel University of Texas at Austin, Swarat Chaudhuri University of Texas at Austin, Işıl Dillig University of Texas at Austin
DOI Media Attached

Accepted Papers

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

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.