POPL 2022
Proceedings of the ACM on Programming Languages, Volume 6, Number POPL

Title Page

Editorial Message

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Quantum Information Effects
Chris Heunen  and Robin Kaarsgaard 
(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  and Santosh Nagarakatte 
(Rutgers University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

SolType: Refinement Types for Arithmetic Overflow in Solidity
Bryan Tan , Benjamin Mariano , Shuvendu K. Lahiri, Isil Dillig , and Yu Feng 
(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  and Luca Padovani 
(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 Choudhury , Jacek Karwowski , and Amr Sabry 
(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 , Minh Nguyen , Tomas Petricek , and Meng Wang 
(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 Kesner 
(Université de Paris, France; CNRS, France; IRIF, France; Institut Universitaire de France, France)

Publisher's Version

A Cost-Aware Logical Framework
Yue Niu , Jonathan Sterling , Harrison Grodin , and Robert Harper 
(Carnegie Mellon University, USA; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Learning Formulas in Finite Variable Logics
Paul Krogmeier  and P. Madhusudan 
(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 Pottier 
(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 Pavlogiannis 
(Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

On Type-Cases, Union Elimination, and Occurrence Typing
Giuseppe Castagna , Mickaël Laurent , Kim Nguyễn , and Matthew Lutze 
(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 , Aws Albarghouthi , Gautam Prakriya , and Somesh Jha 
(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 , 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 Zhang  and Nada Amin 
(University of Waterloo, Canada; Harvard University, USA)

Publisher's Version

Context-Bounded Verification of Thread Pools
Pascal Baumann , Rupak Majumdar , Ramanathan S. Thinniyam , and Georg Zetzsche 
(MPI-SWS, Germany)

Publisher's Version

From Enhanced Coinduction towards Enhanced Induction
Davide Sangiorgi 
(University of Bologna, Italy; Inria, France)

Publisher's Version Archive submitted (300 kB)

Effectful Program Distancing
Ugo Dal Lago  and Francesco Gavazzo 
(University of Bologna, Italy; Inria, France)

Publisher's Version

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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution
Anders Miltner , Adrian Trejo Nuñez , Ana Brendel , Swarat Chaudhuri , and Isil Dillig 
(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 Raad , Luc Maranget , and Viktor Vafeiadis 
(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. Hirsch  and Deepak Garg 
(MPI-SWS, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Certifying Derivation of State Machines from Coroutines
Mirai Ikebuchi, Andres Erbsen , and Adam Chlipala 
(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 , Ling Zhang , Zhong Shao , and Jérémie Koenig 
(Shanghai Jiao Tong University, China; Yale University, USA)

Publisher's Version Published Artifact 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)

Publisher's Version

Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI
Matthew Kolosick, Shravan Narayan , Evan Johnson , Conrad Watt , Michael LeMay , Deepak Garg , Ranjit Jhala , and Deian Stefan 
(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 , Michael Sammler , Simon Spies , Ralf Jung , Hoang-Hai Dang , Robbert Krebbers , Jeehoon Kang , and Derek Dreyer 
(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 , Arthur Azevedo de Amorim, and Marco Gaboardi 
(Boston University, USA)

Publisher's Version

Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
Charles Yuan , Christopher McNally , and Michael Carbin 
(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 Lago  and Francesco Gavazzo 
(University of Bologna, Italy; Inria, France)

Publisher's Version

Observational Equality: Now for Good
Loïc Pujet  and Nicolas Tabareau 
(Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Visibility Reasoning for Concurrent Snapshot Algorithms
Joakim Öhman  and Aleksandar Nanevski 
(IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain)

Publisher's Version Archive submitted (530 kB)

Concurrent Incorrectness Separation Logic
Azalea Raad , Josh Berdine , Derek Dreyer , and Peter W. O'Hearn 
(Imperial College London, UK; Meta, UK; MPI-SWS, Germany; University College London, UK)

Publisher's Version

Relational E-matching
Yihong Zhang , Yisu Remy Wang , Max Willsey , and Zachary Tatlock 
(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 , Jun Sun , 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 , 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  and David Walker 
(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 Jang , Samuel Gélineau , Stefan Monnier , and Brigitte Pientka 
(McGill University, Canada; SimSpace, Canada; Université de Montréal, Canada)

Publisher's Version

Dependently-Typed Data Plane Programming
Matthias Eichholz , Eric Hayden Campbell , Matthias Krebs , Nate Foster , and Mira Mezini 
(TU Darmstadt, Germany; Cornell University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Subcubic Certificates for CFL Reachability
Dmitry Chistikov, Rupak Majumdar , and Philipp Schepper
(University of Warwick, UK; MPI-SWS, Germany; CISPA, Germany)

Publisher's Version

Layered and Object-Based Game Semantics
Arthur Oliveira Vale , Paul-André Melliès , Zhong Shao , Jérémie Koenig , and Léo Stefanesco 
(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 , Gleb Makarchuk , Gagandeep Singh , Markus Püschel, and Martin Vechev 
(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 , Shin-ya Katsumata , and Philip Saville 
(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 , Alejandro Flores-Lamas, Matthew Hague , Zhilei Han , Denghang Hu, Shuanglong Kan, Anthony W. Lin , Philipp Rümmer , and Zhilin Wu 
(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 
(Illinois Institute of Technology, USA)

Publisher's Version 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)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation
Faustyna Krawiec , Simon Peyton Jones , Neel Krishnaswami , Tom Ellis , Richard A. Eisenberg , and Andrew Fitzgibbon 
(University of Cambridge, UK; Microsoft Research, UK; Tweag, France)

Publisher's Version

Truly Stateless, Optimal Dynamic Partial Order Reduction
Michalis Kokologiannakis , Iason Marmanis, Vladimir Gladstein , and Viktor Vafeiadis 
(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 Aiken 
(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  and Benjamin Delaware 
(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  and Dmitrij Szamozvancev 
(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 Jeffrey , James Riely , Mark Batty , Simon Cooksey , Ilya Kaysin , and Anton Podkopaev 
(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 , Gilbert Louis Bernstein , Adam Chlipala , and Jonathan Ragan-Kelley 
(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 , Rem Yang , Gagandeep Singh , and Sasa Misailovic 
(University of Illinois at Urbana-Champaign, USA; VMware, USA)

Publisher's Version

A Separation Logic for Negative Dependence
Jialu Bao, Marco Gaboardi , Justin Hsu , 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 
(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 , Mila Dalla Preda , and Roberto Giacobazzi 
(University of Verona, Italy)

Publisher's Version

Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Functions
Hari Govind V K , Sharon Shoham , and Arie Gurfinkel 
(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 Wu , Jeremy Yallop , and Meng Wang 
(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 , Kris Satya, and Qirun Zhang 
(Georgia Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Software Model-Checking as Cyclic-Proof Search
Takeshi Tsukada  and Hiroshi Unno 
(Chiba University, Japan; University of Tsukuba, Japan; RIKEN AIP, Japan)

Publisher's Version

Logarithm and Program Testing
Kuen-Bang Hou (Favonia)  and Zhuyang Wang 
(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 , Engel Lefaucheux , Joël Ouaknine , David Purser , Anton Varonka , Markus A. Whiteland , and James Worrell 
(MPI-SWS, Germany; University of Oxford, UK)

Publisher's Version