POPL 2022
Proceedings of the ACM on Programming Languages, Volume 6, Number POPL
Powered by
Conference Publishing Consulting

Proceedings of the ACM on Programming Languages, Volume 6, Number POPL, January 16–22, 2022, Philadelphia, PA, USA

POPL – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message

Papers

Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic
Jules JacobsORCID logo, Stephanie BalzerORCID logo, and Robbert KrebbersORCID logo
(Radboud University Nijmegen, Netherlands; Carnegie Mellon University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Quantum Information Effects
Chris Heunen ORCID logo and Robin Kaarsgaard ORCID logo
(University of Edinburgh, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding Modes
Jay P. Lim ORCID logo and Santosh Nagarakatte ORCID logo
(Rutgers University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
SolType: Refinement Types for Arithmetic Overflow in Solidity
Bryan Tan ORCID logo, Benjamin Mariano ORCID logo, Shuvendu K. Lahiri, Isil Dillig ORCID logo, and Yu FengORCID logo
(University of California at Santa Barbara, USA; University of Texas at Austin, USA; Microsoft Research, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Fair Termination of Binary Sessions
Luca Ciccone ORCID logo and Luca PadovaniORCID logo
(University of Turin, Italy)
Publisher's Version Published Artifact Archive submitted (600 kB) Artifacts Available Artifacts Reusable
Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages
Vikraman ChoudhuryORCID logo, Jacek Karwowski ORCID logo, and Amr Sabry ORCID logo
(Indiana University, USA; University of Cambridge, UK; University of Warsaw, Poland)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
Linked Visualisations via Galois Dependencies
Roly Perera ORCID logo, Minh Nguyen ORCID logo, Tomas Petricek ORCID logo, and Meng Wang ORCID logo
(Alan Turing Institute, UK; University of Bristol, UK; University of Kent, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
A Fine-Grained Computational Interpretation of Girard’s Intuitionistic Proof-Nets
Delia KesnerORCID logo
(Université de Paris, France; CNRS, France; IRIF, France; Institut Universitaire de France, France)
Publisher's Version
A Cost-Aware Logical Framework
Yue Niu ORCID logo, Jonathan Sterling ORCID logo, Harrison Grodin ORCID logo, and Robert HarperORCID logo
(Carnegie Mellon University, USA; Aarhus University, Denmark)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Learning Formulas in Finite Variable Logics
Paul Krogmeier ORCID logo and P. MadhusudanORCID logo
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version
A Separation Logic for Heap Space under Garbage Collection
Jean-Marie Madiot and François PottierORCID logo
(Inria, France)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
The Decidability and Complexity of Interleaved Bidirected Dyck Reachability
Adam Husted Kjelstrøm and Andreas PavlogiannisORCID logo
(Aarhus University, Denmark)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
On Type-Cases, Union Elimination, and Occurrence Typing
Giuseppe Castagna ORCID logo, Mickaël Laurent ORCID logo, Kim Nguyễn ORCID logo, and Matthew Lutze ORCID logo
(CNRS, France; Université de Paris, France; Université Paris-Saclay, France)
Publisher's Version Published Artifact Archive submitted (1.1 MB) Artifacts Available Artifacts Reusable
Interval Universal Approximation for Neural Networks
Zi Wang ORCID logo, Aws Albarghouthi ORCID logo, Gautam Prakriya ORCID logo, and Somesh Jha ORCID logo
(University of Wisconsin-Madison, USA; Chinese University of Hong Kong, China; University of Wisconsin, USA)
Publisher's Version Archive submitted (830 kB)
Property-Directed Reachability as Abstract Interpretation in the Monotone Theory
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham ORCID logo, and James R. Wilcox
(Tel Aviv University, Israel; Certora, USA)
Publisher's Version
Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion
Yizhou ZhangORCID logo and Nada Amin ORCID logo
(University of Waterloo, Canada; Harvard University, USA)
Publisher's Version
Context-Bounded Verification of Thread Pools
Pascal Baumann ORCID logo, Rupak Majumdar ORCID logo, Ramanathan S. Thinniyam ORCID logo, and Georg Zetzsche ORCID logo
(MPI-SWS, Germany)
Publisher's Version
From Enhanced Coinduction towards Enhanced Induction
Davide SangiorgiORCID logo
(University of Bologna, Italy; Inria, France)
Publisher's Version Archive submitted (300 kB)
Effectful Program Distancing
Ugo Dal LagoORCID logo and Francesco Gavazzo ORCID logo
(University of Bologna, Italy; Inria, France)
Publisher's Version
VIP: Verifying Real-World C Idioms with Integer-Pointer Casts
Rodolphe Lepigre ORCID logo, Michael Sammler ORCID logo, Kayvan Memarian ORCID logo, Robbert KrebbersORCID logo, Derek DreyerORCID logo, and Peter Sewell ORCID logo
(MPI-SWS, Germany; University of Cambridge, UK; Radboud University Nijmegen, Netherlands)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution
Anders Miltner ORCID logo, Adrian Trejo Nuñez ORCID logo, Ana Brendel ORCID logo, Swarat Chaudhuri ORCID logo, and Isil Dillig ORCID logo
(University of Texas at Austin, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal Stores
Azalea RaadORCID logo, Luc Maranget ORCID logo, and Viktor VafeiadisORCID logo
(Imperial College London, UK; Inria, France; MPI-SWS, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Pirouette: Higher-Order Typed Functional Choreographies
Andrew K. HirschORCID logo and Deepak GargORCID logo
(MPI-SWS, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Certifying Derivation of State Machines from Coroutines
Mirai Ikebuchi, Andres ErbsenORCID logo, and Adam ChlipalaORCID logo
(National Institute of Informatics, Japan; Massachusetts Institute of Technology, USA)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
Verified Compilation of C Programs with a Nominal Memory Model
Yuting Wang ORCID logo, Ling Zhang ORCID logo, Zhong Shao ORCID logo, and Jérémie Koenig ORCID logo
(Shanghai Jiao Tong University, China; Yale University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Semantics for Variational Quantum Programming
Xiaodong Jia ORCID logo, Andre Kornell ORCID logo, Bert Lindenhovius ORCID logo, Michael Mislove ORCID logo, and Vladimir Zamdzhiev ORCID logo
(Hunan University, China; Tulane University, USA; JKU Linz, Austria; Inria, France)
Publisher's Version
Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
Matthew Kolosick, Shravan Narayan ORCID logo, Evan Johnson ORCID logo, Conrad Watt ORCID logo, Michael LeMay ORCID logo, Deepak GargORCID logo, Ranjit JhalaORCID logo, and Deian Stefan ORCID logo
(University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany)
Publisher's Version
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
Lennard Gäher ORCID logo, Michael Sammler ORCID logo, Simon Spies ORCID logo, Ralf JungORCID logo, Hoang-Hai Dang ORCID logo, Robbert KrebbersORCID logo, Jeehoon KangORCID logo, and Derek DreyerORCID logo
(MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
On Incorrectness Logic and Kleene Algebra with Top and Tests
Cheng Zhang ORCID logo, Arthur Azevedo de Amorim, and Marco Gaboardi ORCID logo
(Boston University, USA)
Publisher's Version
Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
Charles Yuan ORCID logo, Christopher McNally ORCID logo, and Michael CarbinORCID logo
(Massachusetts Institute of Technology, USA)
Publisher's Version Published Artifact Archive submitted (690 kB) Artifacts Available Artifacts Reusable
A Relational Theory of Effects and Coeffects
Ugo Dal LagoORCID logo and Francesco Gavazzo ORCID logo
(University of Bologna, Italy; Inria, France)
Publisher's Version
Observational Equality: Now for Good
Loïc Pujet ORCID logo and Nicolas TabareauORCID logo
(Inria, France)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Visibility Reasoning for Concurrent Snapshot Algorithms
Joakim Öhman ORCID logo and Aleksandar Nanevski ORCID logo
(IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain)
Publisher's Version Archive submitted (530 kB)
Concurrent Incorrectness Separation Logic
Azalea RaadORCID logo, Josh Berdine ORCID logo, Derek DreyerORCID logo, and Peter W. O'Hearn ORCID logo
(Imperial College London, UK; Meta, UK; MPI-SWS, Germany; University College London, UK)
Publisher's Version
Relational E-matching
Yihong Zhang ORCID logo, Yisu Remy Wang ORCID logo, Max WillseyORCID logo, and Zachary Tatlock ORCID logo
(University of Washington, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic
Xuan-Bach Le, Shang-Wei Lin ORCID logo, Jun SunORCID logo, and David Sanan
(Nanyang Technological University, Singapore; Singapore Management University, Singapore)
Publisher's Version
Type-Level Programming with Match Types
Olivier Blanvillain, Jonathan Immanuel Brachthäuser ORCID logo, Maxime Kjaer, and Martin Odersky
(EPFL, Switzerland; University of Tübingen, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Safe, Modular Packet Pipeline Programming
Devon Loehr ORCID logo and David Walker ORCID logo
(Princeton University, USA)
Publisher's Version Published Artifact Archive submitted (760 kB) Artifacts Available Artifacts Reusable
Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on Itself
Junyoung JangORCID logo, Samuel GélineauORCID logo, Stefan Monnier ORCID logo, and Brigitte PientkaORCID logo
(McGill University, Canada; SimSpace, Canada; Université de Montréal, Canada)
Publisher's Version
Dependently-Typed Data Plane Programming
Matthias Eichholz ORCID logo, Eric Hayden Campbell ORCID logo, Matthias Krebs ORCID logo, Nate FosterORCID logo, and Mira Mezini ORCID logo
(TU Darmstadt, Germany; Cornell University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Subcubic Certificates for CFL Reachability
Dmitry Chistikov, Rupak Majumdar ORCID logo, and Philipp Schepper
(University of Warwick, UK; MPI-SWS, Germany; CISPA, Germany)
Publisher's Version
Layered and Object-Based Game Semantics
Arthur Oliveira Vale ORCID logo, Paul-André Melliès ORCID logo, Zhong Shao ORCID logo, Jérémie Koenig ORCID logo, and Léo Stefanesco ORCID logo
(Yale University, USA; CNRS, France; Université de Paris, France; MPI-SWS, Germany)
Publisher's Version
PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
Mark Niklas Müller ORCID logo, Gleb Makarchuk ORCID logo, Gagandeep SinghORCID logo, Markus Püschel, and Martin VechevORCID logo
(ETH Zurich, Switzerland; VMware Research, USA; University of Illinois at Urbana-Champaign, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical Relations
Ohad Kammar ORCID logo, Shin-ya Katsumata ORCID logo, and Philip Saville ORCID logo
(University of Edinburgh, UK; National Institute of Informatics, Japan; University of Oxford, UK)
Publisher's Version
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables
Taolue Chen ORCID logo, Alejandro Flores-Lamas, Matthew Hague ORCID logo, Zhilei Han ORCID logo, Denghang Hu, Shuanglong Kan, Anthony W. Lin ORCID logo, Philipp Rümmer ORCID logo, and Zhilin Wu ORCID logo
(Birkbeck University of London, UK; Royal Holloway University of London, UK; Tsinghua University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Static Prediction of Parallel Computation Graphs
Stefan K. Muller ORCID logo
(Illinois Institute of Technology, USA)
Publisher's Version Archive submitted (900 kB)
A Formal Foundation for Symbolic Evaluation with Merging
Sorawee Porncharoenwase ORCID logo, Luke Nelson, Xi Wang, and Emina Torlak ORCID logo
(University of Washington, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation
Faustyna Krawiec ORCID logo, Simon Peyton Jones ORCID logo, Neel Krishnaswami ORCID logo, Tom Ellis ORCID logo, Richard A. Eisenberg ORCID logo, and Andrew Fitzgibbon ORCID logo
(University of Cambridge, UK; Microsoft Research, UK; Tweag, France)
Publisher's Version
Truly Stateless, Optimal Dynamic Partial Order Reduction
Michalis KokologiannakisORCID logo, Iason Marmanis, Vladimir Gladstein ORCID logo, and Viktor VafeiadisORCID logo
(MPI-SWS, Germany; St. Petersburg University, Russia; JetBrains Research, Russia)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
Induction Duality: Primal-Dual Search for Invariants
Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex AikenORCID logo
(VMware Research, USA; Stanford University, USA; Certora, USA; University of Texas at Austin, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Oblivious Algebraic Data Types
Qianchuan Ye ORCID logo and Benjamin DelawareORCID logo
(Purdue University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Profile Inference Revisited
Wenlei He, Julián Mestre, Sergey Pupyrev, Lei Wang, and Hongtao Yu
(Facebook, USA; University of Sydney, Australia)
Publisher's Version
Formal Metatheory of Second-Order Abstract Syntax
Marcelo Fiore ORCID logo and Dmitrij Szamozvancev ORCID logo
(University of Cambridge, UK)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency
Alan JeffreyORCID logo, James RielyORCID logo, Mark Batty ORCID logo, Simon CookseyORCID logo, Ilya KaysinORCID logo, and Anton Podkopaev ORCID logo
(Roblox, USA; DePaul University, USA; University of Kent, UK; JetBrains Research, Russia; University of Cambridge, UK; HSE University, Russia)
Publisher's Version Published Artifact Info Artifacts Available
Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites
Amanda Liu ORCID logo, Gilbert Louis BernsteinORCID logo, Adam ChlipalaORCID logo, and Jonathan Ragan-Kelley ORCID logo
(Massachusetts Institute of Technology, USA; University of California at Berkeley, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
A Dual Number Abstraction for Static Analysis of Clarke Jacobians
Jacob Laurel ORCID logo, Rem Yang ORCID logo, Gagandeep SinghORCID logo, and Sasa MisailovicORCID logo
(University of Illinois at Urbana-Champaign, USA; VMware, USA)
Publisher's Version
A Separation Logic for Negative Dependence
Jialu Bao, Marco Gaboardi ORCID logo, Justin HsuORCID logo, and Joseph Tassarotti
(Cornell University, USA; Boston University, USA; Boston College, USA)
Publisher's Version
Return of CFA: Call-Site Sensitivity Can Be Superior to Object Sensitivity Even for Object-Oriented Programs
Minseok Jeon and Hakjoo Oh ORCID logo
(Korea University, South Korea)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program Analysis
Marco Campion ORCID logo, Mila Dalla PredaORCID logo, and Roberto GiacobazziORCID logo
(University of Verona, Italy)
Publisher's Version
Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Functions
Hari Govind V KORCID logo, Sharon Shoham ORCID logo, and Arie Gurfinkel ORCID logo
(University of Waterloo, Canada; Tel Aviv University, Israel)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Staging with Class: A Specification for Typed Template Haskell
Ningning Xie, Matthew Pickering, Andres Löh, Nicolas WuORCID logo, Jeremy YallopORCID logo, and Meng Wang ORCID logo
(University of Cambridge, UK; Well-Typed LLP, UK; Imperial College London, UK; University of Bristol, UK)
Publisher's Version
Efficient Algorithms for Dynamic Bidirected Dyck-Reachability
Yuanbo Li ORCID logo, Kris Satya, and Qirun Zhang ORCID logo
(Georgia Institute of Technology, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Software Model-Checking as Cyclic-Proof Search
Takeshi Tsukada ORCID logo and Hiroshi UnnoORCID logo
(Chiba University, Japan; University of Tsukuba, Japan; RIKEN AIP, Japan)
Publisher's Version
Logarithm and Program Testing
Kuen-Bang Hou (Favonia)ORCID logo and Zhuyang WangORCID logo
(University of Minnesota, USA)
Publisher's Version Published Artifact Archive submitted (540 kB) Artifacts Available Artifacts Reusable
What’s Decidable about Linear Loops?
Toghrul Karimov ORCID logo, Engel Lefaucheux ORCID logo, Joël Ouaknine ORCID logo, David Purser ORCID logo, Anton Varonka ORCID logo, Markus A. Whiteland ORCID logo, and James Worrell ORCID logo
(MPI-SWS, Germany; University of Oxford, UK)
Publisher's Version

proc time: 11.46