POPL – Journal Issue

Artifacts Reusable Article: popl22main-p6-p doi:10.1145/3498662

Quantum Information Effects
Chris Heunen and Robin Kaarsgaard
(University of Edinburgh, UK)

Artifacts Reusable Article: popl22main-p9-p doi:10.1145/3498663

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)

Artifacts Reusable Article: popl22main-p25-p doi:10.1145/3498664

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)

Artifacts Reusable Article: popl22main-p27-p doi:10.1145/3498665

Fair Termination of Binary Sessions
Luca Ciccone and Luca Padovani
(University of Turin, Italy)

Archive submitted (600 kB)

Artifacts Reusable Article: popl22main-p30-p doi:10.1145/3498666

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)

Artifacts Reusable Article: popl22main-p31-p doi:10.1145/3498667

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)

Artifacts Reusable Article: popl22main-p34-p doi:10.1145/3498668

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 Article: popl22main-p42-p doi:10.1145/3498669

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

Artifacts Reusable Article: popl22main-p47-p doi:10.1145/3498670

Learning Formulas in Finite Variable Logics
Paul Krogmeier and P. Madhusudan
(University of Illinois at Urbana-Champaign, USA)

Publisher's Version Article: popl22main-p48-p doi:10.1145/3498671

A Separation Logic for Heap Space under Garbage Collection
Jean-Marie Madiot and François Pottier
(Inria, France)

Artifacts Reusable Article: popl22main-p49-p doi:10.1145/3498672

The Decidability and Complexity of Interleaved Bidirected Dyck Reachability
Adam Husted Kjelstrøm and Andreas Pavlogiannis
(Aarhus University, Denmark)

Artifacts Reusable Article: popl22main-p55-p doi:10.1145/3498673

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)

Archive submitted (1.1 MB)

Artifacts Reusable Article: popl22main-p58-p doi:10.1145/3498674

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)

Archive submitted (830 kB) Article: popl22main-p61-p doi:10.1145/3498675

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 Article: popl22main-p65-p doi:10.1145/3498676

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 Article: popl22main-p66-p doi:10.1145/3498677

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

Publisher's Version Article: popl22main-p90-p doi:10.1145/3498678

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

Archive submitted (300 kB) Article: popl22main-p93-p doi:10.1145/3498679

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

Publisher's Version Article: popl22main-p94-p doi:10.1145/3498680

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)

Artifacts Reusable Article: popl22main-p95-p doi:10.1145/3498681

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)

Artifacts Reusable Article: popl22main-p124-p doi:10.1145/3498682

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)

Artifacts Reusable Article: popl22main-p126-p doi:10.1145/3498683

Pirouette: Higher-Order Typed Functional Choreographies
Andrew K. Hirsch and Deepak Garg
(MPI-SWS, Germany)

Artifacts Reusable Article: popl22main-p131-p doi:10.1145/3498684

Certifying Derivation of State Machines from Coroutines
Mirai Ikebuchi, Andres Erbsen, and Adam Chlipala
(National Institute of Informatics, Japan; Massachusetts Institute of Technology, USA)

Artifacts Reusable Article: popl22main-p137-p doi:10.1145/3498685

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)

Artifacts Reusable Article: popl22main-p143-p doi:10.1145/3498686

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 Article: popl22main-p149-p doi:10.1145/3498687

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 Article: popl22main-p151-p doi:10.1145/3498688

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)

Artifacts Reusable Article: popl22main-p158-p doi:10.1145/3498689

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 Article: popl22main-p160-p doi:10.1145/3498690

Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
Charles Yuan, Christopher McNally, and Michael Carbin
(Massachusetts Institute of Technology, USA)

Archive submitted (690 kB)

Artifacts Reusable Article: popl22main-p167-p doi:10.1145/3498691

A Relational Theory of Effects and Coeffects
Ugo Dal Lago and Francesco Gavazzo
(University of Bologna, Italy; Inria, France)

Publisher's Version Article: popl22main-p168-p doi:10.1145/3498692

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

Artifacts Reusable Article: popl22main-p191-p doi:10.1145/3498693

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

Archive submitted (530 kB) Article: popl22main-p206-p doi:10.1145/3498694

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 Article: popl22main-p233-p doi:10.1145/3498695

Relational E-matching
Yihong Zhang, Yisu Remy Wang, Max Willsey, and Zachary Tatlock
(University of Washington, USA)

Artifacts Reusable Article: popl22main-p244-p doi:10.1145/3498696

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 Article: popl22main-p247-p doi:10.1145/3498697

Type-Level Programming with Match Types
Olivier Blanvillain, Jonathan Immanuel Brachthäuser, Maxime Kjaer, and Martin Odersky
(EPFL, Switzerland; University of Tübingen, Germany)

Artifacts Reusable Article: popl22main-p258-p doi:10.1145/3498698

Safe, Modular Packet Pipeline Programming
Devon Loehr and David Walker
(Princeton University, USA)

Archive submitted (760 kB)

Artifacts Reusable Article: popl22main-p275-p doi:10.1145/3498699

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 Article: popl22main-p294-p doi:10.1145/3498700

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

Artifacts Functional Article: popl22main-p311-p doi:10.1145/3498701

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

Publisher's Version Article: popl22main-p322-p doi:10.1145/3498702

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 Article: popl22main-p327-p doi:10.1145/3498703

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)

Artifacts Reusable Article: popl22main-p329-p doi:10.1145/3498704

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 Article: popl22main-p331-p doi:10.1145/3498705

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)

Artifacts Reusable Article: popl22main-p350-p doi:10.1145/3498707

Static Prediction of Parallel Computation Graphs
Stefan K. Muller
(Illinois Institute of Technology, USA)

Archive submitted (900 kB) Article: popl22main-p383-p doi:10.1145/3498708

A Formal Foundation for Symbolic Evaluation with Merging
Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak
(University of Washington, USA)

Artifacts Reusable Article: popl22main-p390-p doi:10.1145/3498709

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 Article: popl22main-p397-p doi:10.1145/3498710

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)

Artifacts Reusable Article: popl22main-p424-p doi:10.1145/3498711

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)

Artifacts Functional Article: popl22main-p428-p doi:10.1145/3498712

Oblivious Algebraic Data Types
Qianchuan Ye and Benjamin Delaware
(Purdue University, USA)

Artifacts Reusable Article: popl22main-p429-p doi:10.1145/3498713

Profile Inference Revisited
Wenlei He, Julián Mestre, Sergey Pupyrev, Lei Wang, and Hongtao Yu
(Facebook, USA; University of Sydney, Australia)

Publisher's Version Article: popl22main-p431-p doi:10.1145/3498714

Formal Metatheory of Second-Order Abstract Syntax
Marcelo Fiore and Dmitrij Szamozvancev
(University of Cambridge, UK)

Artifacts Reusable Article: popl22main-p437-p doi:10.1145/3498715

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)

Artifacts Available Article: popl22main-p459-p doi:10.1145/3498716

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)

Artifacts Reusable Article: popl22main-p523-p doi:10.1145/3498717

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 Article: popl22main-p542-p doi:10.1145/3498718

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 Article: popl22main-p550-p doi:10.1145/3498719

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)

Artifacts Reusable Article: popl22main-p586-p doi:10.1145/3498720

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 Article: popl22main-p597-p doi:10.1145/3498721

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)

Artifacts Reusable Article: popl22main-p629-p doi:10.1145/3498722

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 Article: popl22main-p706-p doi:10.1145/3498723

Efficient Algorithms for Dynamic Bidirected Dyck-Reachability
Yuanbo Li, Kris Satya, and Qirun Zhang
(Georgia Institute of Technology, USA)

Artifacts Reusable Article: popl22main-p725-p doi:10.1145/3498724

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 Article: popl22main-p736-p doi:10.1145/3498725

Logarithm and Program Testing
Kuen-Bang Hou (Favonia) and Zhuyang Wang
(University of Minnesota, USA)

Archive submitted (540 kB)