OOPSLA1 2024
Proceedings of the ACM on Programming Languages, Volume 8, Number OOPSLA1

Title Page

Editorial Message

Quantum Control Machine: The Limits of Control Flow in Quantum Programming
Charles Yuan, Agnes Villanyi, and Michael Carbin
(Massachusetts Institute of Technology, USA)

Publisher's Version Published Artifact Archive submitted (430 kB) Artifacts Available Artifacts Reusable Results Reproduced

Profiling Programming Language Learning
Will Crichton and Shriram Krishnamurthi
(Brown University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Synthetiq: Fast and Versatile Quantum Circuit Synthesis
Anouk Paradis, Jasper Dekoninck, Benjamin Bichsel, and Martin Vechev
(ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

A Learning-Based Approach to Static Program Slicing
Aashish Yadavally, Yi Li, Shaohua Wang, and Tien N. Nguyen
(University of Texas, Dallas, USA; Central University of Finance and Economics, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Finding Cross-Rule Optimization Bugs in Datalog Engines
Chi Zhang, Linzhang Wang, and Manuel Rigger
(Nanjing University, China; National University of Singapore, Singapore)

Publisher's Version Published Artifact Archive submitted (460 kB) Info Artifacts Available Artifacts Functional Results Reproduced

UniSparse: An Intermediate Language for General Sparse Format Customization
Jie Liu, Zhongyuan Zhao, Zijian Ding, Benjamin Brock, Hongbo Rong, and Zhiru Zhang
(Cornell University, USA; University of California at Los Angeles, Los Angeles, USA; Intel, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Cocoon: Static Information Flow Control in Rust
Ada Lamba, Max Taylor, Vincent Beardsley, Jacob Bambeck, Michael D. Bond, and Zhiqiang Lin
(Ohio State University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

Fulfilling OCaml Modules with Transparency
Blaudeau Clement, Didier Rémy, and Gabriel Radanne
(Inria, France; Université de Paris Cité, France)

Publisher's Version Archive submitted (630 kB)

HOL4P4: Mechanized Small-Step Semantics for P4
Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, and Mads Dam
(KTH Royal Institute of Technology, Sweden; Saab, Sweden)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Compiling Recurrences over Dense and Sparse Arrays
Shiv Sundram, Muhammad Usman Tariq, and Fredrik Kjolstad
(Stanford University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
Noam Zilberstein, Angelina Saliling, and Alexandra Silva
(Cornell University, USA)

Publisher's Version

Newtonian Program Analysis of Probabilistic Programs
Di Wang and Thomas Reps
(Peking University, China; University of Wisconsin, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Identifying and Correcting Programming Language Behavior Misconceptions
Kuang-Chen Lu and Shriram Krishnamurthi
(Brown University, USA)

Publisher's Version Published Artifact Archive submitted (1.1 MB) Artifacts Available Artifacts Reusable Results Reproduced

Quantitative Bounds on Resource Usage of Probabilistic Programs
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Đorđe Žikelić
(IST Austria, Austria; Hong Kong University of Science and Technology, China; Lancaster University Leipzig, Germany; Singapore Management University, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

CYCLE: Learning to Self-Refine the Code Generation
Yangruibo Ding, Marcus J. Min, Gail Kaiser, and Baishakhi Ray
(Columbia University, USA)

Publisher's Version

AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects
Wolf Honoré, Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, and Zhong Shao
(Yale University, USA; Northeastern University, USA; Inha University, South Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

PROMPT: A Fast and Extensible Memory Profiling Framework
Ziyang Xu, Yebin Chon, Yian Su, Zujun Tan, Sotiris Apostolakis, Simone Campanoni, and David I. August
(Princeton University, USA; Northwestern University, USA; Google, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Enhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach
Haonan Li, Yu Hao, Yizhuo Zhai, and Zhiyun Qian
(University of California at Riverside, Riverside, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional

Evaluating the Effectiveness of Deep Learning Models for Foundational Program Analysis Tasks
Qian Chen, Chenyang Yu, Ruyan Liu, Chi Zhang, Yu Wang, Ke Wang, Ting Su, and Linzhang Wang
(Nanjing University, China; Visa Research, USA; East China Normal University, China)

Publisher's Version Archive submitted (450 kB)

Inductive Diagrams for Causal Reasoning
Jonathan Castello, Patrick Redmond, and Lindsey Kuper
(University of California at Santa Cruz, Santa Cruz, USA)

Publisher's Version Info

Quarl: A Learning-Based Quantum Circuit Optimizer
Zikun Li, Jinjun Peng, Yixuan Mei, Sina Lin, Yi Wu, Oded Padon, and Zhihao Jia
(Carnegie Mellon University, USA; Columbia University, USA; Microsoft, USA; Tsinghua University, China; VMware Research, USA)

Publisher's Version Published Artifact Artifacts Available

Qualifying System F_<:: Some Terms and Conditions May Apply
Edward Lee, Yaoyu Zhao, Ondřej Lhoták, James You, Kavin Satheeskumar, and Jonathan Immanuel Brachthäuser
(University of Waterloo, Canada; EPFL, Lausanne, Switzerland; University of Tübingen, Tübingen, Germany)

Publisher's Version Published Artifact Archive submitted (290 kB) Artifacts Available Artifacts Reusable Results Reproduced

Forge: A Tool and Language for Teaching Formal Methods
Tim Nelson, Ben Greenman, Siddhartha Prasad, Tristan Dyer, Ethan Bove, Qianfan Chen, Charles Cutting, Thomas Del Vecchio, Sidney LeVine, Julianne Rudner, Ben Ryjikov, Alexander Varga, Andrew Wagner, Luke West, and Shriram Krishnamurthi
(Brown University, USA; University of Utah, USA; Stashpad, USA; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Design and Implementation of an Aspect-Oriented C Programming Language
Zhe Chen, Yunlong Zhu, and Zhemin Wang
(Nanjing University of Aeronautics and Astronautics, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization
Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, and Andrew M. Wells
(University of Pennsylvania, USA; Amazon Web Services, USA; Unaffiliated, USA; University of Maryland, USA)

Publisher's Version Artifacts Reusable Results Reproduced

Persimmon: Nested Family Polymorphism with Extensible Variant Types
Anastasiya Kravchuk-Kirilyuk, Gary Feng, Jonas Iskander, Yizhou Zhang, and Nada Amin
(Harvard University, USA; University of Waterloo, Canada)

Publisher's Version Published Artifact Archive submitted (2.4 MB) Artifacts Available Artifacts Reusable Results Reproduced

Hydra: Generalizing Peephole Optimizations with Program Synthesis
Manasij Mukherjee and John Regehr
(University of Utah, USA)

Publisher's Version

Multiverse Notebook: Shifting Data Scientists to Time Travelers
Shigeyuki Sato and Tomoki Nakamaru
(University of Electro-Communications, Japan; University of Tokyo, Japan)

Publisher's Version Info Artifacts Functional Results Reproduced

Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs
Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, and Gabriele Vanoni
(Centre Inria d’Université Côte d’Azur, France; MPI-SP, Germany; IMDEA Software Institute, Spain; University of Innsbruck, Austria)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Accurate Data Race Prediction in the Linux Kernel through Sparse Fourier Learning
Gabriel Ryan, Burcu Cetin, Yongwhan Lim, and Suman Jana
(Columbia University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

TorchQL: A Programming Framework for Integrity Constraints in Machine Learning
Aaditya Naik, Adam Stein, Yinjun Wu, Mayur Naik, and Eric Wong
(University of Pennsylvania, USA)

Publisher's Version Published Artifact Archive submitted (1.1 MB) Artifacts Available

Gradually Typed Languages Should Be Vigilant!
Olek Gierczak, Lucy Menon, Christos Dimoulas, and Amal Ahmed
(Northeastern University, USA; Northwestern University, USA)

Publisher's Version Archive submitted (830 kB) Info

Distributions for Compositionally Differentiating Parametric Discontinuities
Jesse Michel, Kevin Mu, Xuanda Yang, Sai Praveen Bangaru, Elias Rojas Collins, Gilbert Bernstein, Jonathan Ragan-Kelley, Michael Carbin, and Tzu-Mao Li
(Massachusetts Institute of Technology, USA; University of Washington, USA; University of California at San Diego, San Diego, USA)

Publisher's Version Archive submitted (620 kB)

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase, and Joost-Pieter Katoen
(RWTH Aachen University, Aachen, Germany; Zhejiang University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Learning Abstraction Selection for Bayesian Program Analysis
Yifan Zhang, Yuanfeng Shi, and Xin Zhang
(Peking University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Deriving Dependently-Typed OOP from First Principles
David Binder, Ingo Skupin, Tim Süberkrüb, and Klaus Ostermann
(University of Tübingen, Tübingen, Germany; Aleph Alpha, Germany)

Publisher's Version Published Artifact Archive submitted (110 kB) Info Artifacts Available Artifacts Reusable Results Reproduced

Verification of Neural Networks’ Global Robustness
Anan Kabaha and Dana Drachsler Cohen
(Technion, Israel)

Publisher's Version

Functional Ownership through Fractional Uniqueness
Daniel Marshall and Dominic Orchard
(University of Kent, United Kingdom; University of Cambridge, United Kingdom)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints
Yang He, Pinhan Zhao, Xinyu Wang, and Yuepeng Wang
(Simon Fraser University, Canada; University of Michigan, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

PyDex: Repairing Bugs in Introductory Python Assignments using LLMs
Jialu Zhang, José Pablo Cambronero, Sumit Gulwani, Vu Le, Ruzica Piskac, Gustavo Soares, and Gust Verbruggen
(University of Waterloo, Canada; Microsoft, USA; Yale University, USA; Microsoft, Belgium)

Publisher's Version

Seneca: Taint-Based Call Graph Construction for Java Object Deserialization
Joanna C. S. Santos, Mehdi Mirakhorli, and Ali Shokri
(University of Notre Dame, USA; University of Hawaii, Manoa, USA; Virginia Tech, USA)

Publisher's Version

A Pure Demand Operational Semantics with Applications to Program Analysis
Scott Smith and Robert Zhang
(Johns Hopkins University, USA)

Publisher's Version Published Artifact Archive submitted (1.1 MB) Artifacts Available Artifacts Reusable Results Reproduced

Degrees of Separation: A Flexible Type System for Safe Concurrency
Yichen Xu, Aleksander Boruch-Gruszecki, and Martin Odersky
(EPFL, Lausanne, Switzerland)

Publisher's Version Archive submitted (1.7 MB)

ParDiff: Practical Static Differential Analysis of Network Protocol Parsers
Mingwei Zheng, Qingkai Shi, Xuwei Liu, Xiangzhe Xu, Le Yu, Congyu Liu, Guannan Wei, and Xiangyu Zhang
(Purdue University, USA)

Publisher's Version

A Constraint Solving Approach to Parikh Images of Regular Languages
Amanda Stjerna and Philipp Rümmer
(Uppsala University, Uppsala, Sweden; University of Regensburg, Regensburg, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

PP-CSA: Practical Privacy-Preserving Software Call Stack Analysis
Zhaoyu Wang, Pingchuan Ma, Huaijin Wang, and Shuai Wang
(Hong Kong University of Science and Technology, China)

Publisher's Version

Scenario-Based Proofs for Concurrent Objects
Constantin Enea and Eric Koskinen
(LIX - CNRS - École Polytechnique, France; Stevens Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

Mechanizing the CMP Abstraction for Parameterized Verification
Yongjian Li, Bohua Zhan, and Jun Pang
(Institute of Software at Chinese Academy of Sciences, China; University of Luxembourg, Luxembourg)

Publisher's Version Artifacts Functional Results Reproduced

Message-Observing Sessions
Ryan Kavanagh and Brigitte Pientka
(Université du Québec à Montréal, Canada; McGill University, Canada)

Publisher's Version

Understanding and Finding Java Decompiler Bugs
Yifei Lu, Weidong Hou, Minxue Pan, Xuandong Li, and Zhendong Su
(Nanjing University, China; ETH Zurich, Switzerland)

Publisher's Version

Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation
Qianchuan Ye and Benjamin Delaware
(Purdue University, USA)

Publisher's Version Published Artifact Archive submitted (540 kB) Artifacts Available Artifacts Reusable Results Reproduced

Iterative-Epoch Online Cycle Elimination for Context-Free Language Reachability
Pei Xu, Yuxiang Lei, Yulei Sui, and Jingling Xue
(University of Technology Sydney, Australia; UNSW, Sydney, Australia)

Publisher's Version

Modeling Dynamic (De)Allocations of Local Memory for Translation Validation
Abhishek Rose and Sorav Bansal
(IIT Delhi, India)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional