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 Jacobs, Stephanie Balzer, and Robbert Krebbers
(Radboud University Nijmegen, Netherlands; Carnegie Mellon University, USA)
Article Search Artifacts Available Artifacts Reusable
Quantum Information Effects
Chris Heunen and Robin Kaarsgaard
(University of Edinburgh, UK)
Article Search 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 NagarakatteORCID logo
(Rutgers University, USA)
Article Search Artifacts Available Artifacts Reusable
SolType: Refinement Types for Arithmetic Overflow in Solidity
Bryan Tan ORCID logo, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig ORCID logo, and Yu Feng
(University of California at Santa Barbara, USA; University of Texas at Austin, USA; Microsoft Research, USA)
Article Search Artifacts Available Artifacts Reusable
Fair Termination of Binary Sessions
Luca Ciccone ORCID logo and Luca PadovaniORCID logo
(University of Turin, Italy)
Preprint 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)
Preprint 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)
Article Search 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)
Article Search
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)
Article Search 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)
Article Search
A Separation Logic for Heap Space under Garbage Collection
Jean-Marie Madiot and François PottierORCID logo
(Inria, France)
Article Search Artifacts Available Artifacts Reusable
The Decidability and Complexity of Interleaved Bidirected Dyck Reachability
Adam Husted Kjelstrøm and Andreas PavlogiannisORCID logo
(Aarhus University, Denmark)
Article Search 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)
Article Search 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)
Preprint 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)
Article Search
Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion
Yizhou Zhang ORCID logo and Nada Amin
(University of Waterloo, Canada; Harvard University, USA)
Article Search
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)
Article Search
From Enhanced Coinduction towards Enhanced Induction
Davide SangiorgiORCID logo
(University of Bologna, Italy)
Article Search Archive submitted (300 kB)
Effectful Program Distancing
Ugo Dal LagoORCID logo and Francesco Gavazzo
(University of Bologna, Italy; Inria, France)
Article Search
VIP: Verifying Real-World C Idioms with Integer-Pointer Casts
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell
(MPI-SWS, Germany; University of Cambridge, UK; Radboud University Nijmegen, Netherlands)
Article Search 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)
Article Search 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)
Article Search Artifacts Available Artifacts Reusable
Pirouette: Higher-Order Typed Functional Choreographies
Andrew K. HirschORCID logo and Deepak GargORCID logo
(MPI-SWS, Germany)
Preprint Artifacts Available Artifacts Reusable
Certifying Derivation of State Machines from Coroutines
Mirai Ikebuchi, Andres ErbsenORCID logo, and Adam ChlipalaORCID logo
(Massachusetts Institute of Technology, USA)
Article Search 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)
Article Search Artifacts Available Artifacts Reusable
Semantics for Variational Quantum Programming
Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev
(Hunan University, China; Tulane University, USA; JKU Linz, Austria; Inria, France; LORIA, France; University of Lorraine, France)
Preprint
Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay ORCID logo, Deepak GargORCID logo, Ranjit Jhala, and Deian Stefan
(University of California at San Diego, USA; University of Cambridge, UK; Intel Labs, USA; MPI-SWS, Germany)
Article Search
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon KangORCID logo, and Derek Dreyer
(MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; KAIST, South Korea)
Article Search 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
(Boston University, USA)
Article Search
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)
Article Search Archive submitted (690 kB) Artifacts Available Artifacts Reusable
A Relational Theory of Effects and Coeffects
Ugo Dal LagoORCID logo and Francesco Gavazzo
(University of Bologna, Italy; Inria, France)
Article Search
Observational Equality: Now for Good
Loïc Pujet and Nicolas TabareauORCID logo
(Inria, France)
Article Search 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)
Article Search Archive submitted (530 kB)
Concurrent Incorrectness Separation Logic
Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn
(Imperial College London, UK; Facebook, UK; MPI-SWS, Germany; University College London, UK)
Article Search
Relational E-matching
Yihong Zhang, Yisu Remy Wang, Max WillseyORCID logo, and Zachary Tatlock
(University of Washington, USA)
Article Search 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, Jun SunORCID logo, and David Sanan
(Nanyang Technological University, Singapore; Singapore Management University, Singapore)
Article Search
Type-Level Programming with Match Types
Olivier Blanvillain, Jonathan Immanuel Brachthäuser ORCID logo, Maxime Kjaer, and Martin Odersky
(EPFL, Switzerland)
Article Search Artifacts Available Artifacts Reusable
Safe, Modular Packet Pipeline Programming
Devon Loehr ORCID logo and David Walker
(Princeton University, USA)
Article Search 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, n.n.; Université de Montréal, Canada)
Article Search
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)
Article Search 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)
Article Search
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)
Article Search
PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
Mark Niklas Müller, Gleb Makarchuk ORCID logo, Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland; VMware Research, USA; University of Illinois at Urbana-Champaign, USA)
Article Search 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)
Article Search
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)
Article Search Artifacts Available Artifacts Reusable
Static Prediction of Parallel Computation Graphs
Stefan K. Muller ORCID logo
(Illinois Institute of Technology, USA)
Article Search Archive submitted (900 kB)
A Formal Foundation for Symbolic Evaluation with Merging
Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak
(University of Washington, USA)
Article Search Artifacts Available Artifacts Reusable
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation
Faustyna Krawiec ORCID logo, Simon Peyton-Jones, 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)
Article Search
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)
Article Search 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 Aiken
(VMware Research, USA; Stanford University, USA; Certora, USA; University of Texas at Austin, USA)
Article Search Artifacts Available Artifacts Functional
Oblivious Algebraic Data Types
Qianchuan Ye and Benjamin Delaware
(Purdue University, USA)
Article Search 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)
Preprint
Formal Metatheory of Second-Order Abstract Syntax
Marcelo Fiore ORCID logo and Dmitrij Szamozvancev ORCID logo
(University of Cambridge, UK)
Article Search 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)
Article Search Info Artifacts Available
Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites
Amanda Liu ORCID logo, Gilbert Louis Bernstein, Adam ChlipalaORCID logo, and Jonathan Ragan-Kelley ORCID logo
(Massachusetts Institute of Technology, USA; University of California at Berkeley, USA)
Article Search Artifacts Available Artifacts Reusable
A Dual Number Abstraction for Static Analysis of Clarke Jacobians
Jacob Laurel, Rem Yang, Gagandeep Singh, and Sasa Misailovic
(University of Illinois at Urbana-Champaign, USA; VMware, USA)
Article Search
A Separation Logic for Negative Dependence
Jialu Bao, Marco Gaboardi, Justin Hsu, and Joseph Tassarotti
(Cornell University, USA; Boston University, USA; Boston College, USA)
Preprint
Return of CFA: Call-Site Sensitivity Can Be Superior to Object Sensitivity Even for Object-Oriented Programs
Minseok Jeon and Hakjoo Oh
(Korea University, South Korea)
Article Search 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)
Article Search
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)
Article Search Artifacts Available Artifacts Reusable
Staging with Class: A Specification for Typed Template Haskell
Ningning Xie, Matthew Pickering, Andres Löh, Nicolas WuORCID logo, Jeremy Yallop, and Meng Wang ORCID logo
(University of Cambridge, UK; Well-Typed LLP, UK; Imperial College London, UK; University of Bristol, UK)
Article Search
Efficient Algorithms for Dynamic Bidirected Dyck-Reachability
Yuanbo Li, Kris Satya, and Qirun Zhang
(Georgia Institute of Technology, USA)
Article Search Artifacts Available Artifacts Reusable
Software Model-Checking as Cyclic-Proof Search
Takeshi Tsukada ORCID logo and Hiroshi Unno ORCID logo
(Chiba University, Japan; University of Tsukuba, Japan)
Article Search
Logarithm and Program Testing
Kuen-Bang Hou (Favonia)ORCID logo and Zhuyang WangORCID logo
(University of Minnesota, USA)
Article Search Archive submitted (540 kB) Artifacts Available Artifacts Reusable
What’s Decidable about Linear Loops?
Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell
(MPI-SWS, Germany; University of Oxford, UK)
Article Search

proc time: 14.54