OOPSLA1 2024
Proceedings of the ACM on Programming Languages, Volume 8, Number OOPSLA1
Powered by
Conference Publishing Consulting

Proceedings of the ACM on Programming Languages, Volume 8, Number OOPSLA1, October 20–25, 2024, Pasadena, CA, USA

OOPSLAA – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message

Papers

Quantum Control Machine: The Limits of Control Flow in Quantum Programming
Charles Yuan ORCID logo, Agnes Villanyi ORCID logo, and Michael CarbinORCID logo
(Massachusetts Institute of Technology, USA)
Published Artifact Archive submitted (430 kB) Artifacts Available Artifacts Reusable Results Reproduced
Profiling Programming Language Learning
Will Crichton ORCID logo and Shriram Krishnamurthi ORCID logo
(Brown University, USA)
Published Artifact Artifacts Available Artifacts Reusable Results Reproduced
Synthetiq: Fast and Versatile Quantum Circuit Synthesis
Anouk Paradis ORCID logo, Jasper Dekoninck ORCID logo, Benjamin Bichsel ORCID logo, and Martin VechevORCID logo
(ETH Zurich, Switzerland)
Published Artifact Artifacts Available Artifacts Reusable Results Reproduced
A Learning-Based Approach to Static Program Slicing
Aashish Yadavally ORCID logo, Yi Li ORCID logo, Shaohua Wang ORCID logo, and Tien N. Nguyen ORCID logo
(University of Texas, Dallas, USA; Central University of Finance and Economics, China)
Published Artifact Artifacts Available Artifacts Reusable Results Reproduced
Finding Cross-Rule Optimization Bugs in Datalog Engines
Chi Zhang ORCID logo, Linzhang Wang ORCID logo, and Manuel Rigger ORCID logo
(Nanjing University, China; National University of Singapore, Singapore)
Published Artifact Archive submitted (460 kB) Info Artifacts Available Artifacts Functional Results Reproduced
UniSparse: An Intermediate Language for General Sparse Format Customization
Jie LiuORCID logo, Zhongyuan Zhao ORCID logo, Zijian Ding ORCID logo, Benjamin Brock ORCID logo, Hongbo Rong ORCID logo, and Zhiru Zhang ORCID logo
(Cornell University, USA; University of California at Los Angeles, Los Angeles, USA; Intel, USA)
Published Artifact Artifacts Available Artifacts Functional
Cocoon: Static Information Flow Control in Rust
Ada Lamba ORCID logo, Max Taylor ORCID logo, Vincent Beardsley ORCID logo, Jacob Bambeck ORCID logo, Michael D. Bond ORCID logo, and Zhiqiang Lin ORCID logo
(Ohio State University, USA)
Published Artifact Artifacts Available Artifacts Functional Results Reproduced
Fulfilling OCaml Modules with Transparency
Blaudeau ClementORCID logo, Didier RémyORCID logo, and Gabriel RadanneORCID logo
(Inria, France; Université de Paris Cité, France)
Archive submitted (630 kB)
HOL4P4: Mechanized Small-Step Semantics for P4
Anoud Alshnakat ORCID logo, Didrik Lundberg ORCID logo, Roberto Guanciale ORCID logo, and Mads Dam ORCID logo
(KTH Royal Institute of Technology, Sweden; Saab, Sweden)
Published Artifact Artifacts Available Artifacts Reusable Results Reproduced
Compiling Recurrences over Dense and Sparse Arrays
Shiv Sundram ORCID logo, Muhammad Usman Tariq ORCID logo, and Fredrik Kjolstad ORCID logo
(Stanford University, USA)
Published Artifact Artifacts Available Artifacts Functional Results Reproduced
Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
Noam Zilberstein ORCID logo, Angelina Saliling ORCID logo, and Alexandra Silva ORCID logo
(Cornell University, USA)
Newtonian Program Analysis of Probabilistic Programs
Di Wang ORCID logo and Thomas RepsORCID logo
(Peking University, China; University of Wisconsin, USA)
Published Artifact Artifacts Available Artifacts Reusable Results Reproduced
Identifying and Correcting Programming Language Behavior Misconceptions
Kuang-Chen Lu ORCID logo and Shriram Krishnamurthi ORCID logo
(Brown University, USA)
Published Artifact Archive submitted (1.1 MB) Artifacts Available Artifacts Reusable Results Reproduced
Quantitative Bounds on Resource Usage of Probabilistic Programs
Krishnendu Chatterjee ORCID logo, Amir Kafshdar Goharshady ORCID logo, Tobias Meggendorfer ORCID logo, and Đorđe Žikelić ORCID logo
(IST Austria, Austria; Hong Kong University of Science and Technology, China; Lancaster University Leipzig, Germany; Singapore Management University, Singapore)
Published Artifact Artifacts Available Artifacts Reusable Results Reproduced
CYCLE: Learning to Self-Refine the Code Generation
Yangruibo DingORCID logo, Marcus J. Min ORCID logo, Gail Kaiser ORCID logo, and Baishakhi RayORCID logo
(Columbia University, USA)
AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects
Wolf Honoré ORCID logo, Longfei Qiu ORCID logo, Yoonseung Kim ORCID logo, Ji-Yong Shin ORCID logo, Jieung Kim ORCID logo, and Zhong Shao ORCID logo
(Yale University, USA; Northeastern University, USA; Inha University, South Korea)
Published Artifact Artifacts Available Artifacts Functional
PROMPT: A Fast and Extensible Memory Profiling Framework
Ziyang Xu ORCID logo, Yebin Chon ORCID logo, Yian Su ORCID logo, Zujun Tan ORCID logo, Sotiris Apostolakis ORCID logo, Simone Campanoni ORCID logo, and David I. August ORCID logo
(Princeton University, USA; Northwestern University, USA; Google, USA)
Published Artifact Artifacts Available Artifacts Reusable
Enhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach
Haonan Li ORCID logo, Yu Hao ORCID logo, Yizhuo Zhai ORCID logo, and Zhiyun Qian ORCID logo
(University of California at Riverside, Riverside, USA)
Published Artifact Info Artifacts Available Artifacts Functional
Evaluating the Effectiveness of Deep Learning Models for Foundational Program Analysis Tasks
Qian Chen ORCID logo, Chenyang Yu ORCID logo, Ruyan Liu ORCID logo, Chi Zhang ORCID logo, Yu Wang ORCID logo, Ke Wang ORCID logo, Ting Su ORCID logo, and Linzhang Wang ORCID logo
(Nanjing University, China; Visa Research, USA; East China Normal University, China)
Archive submitted (450 kB)
Inductive Diagrams for Causal Reasoning
Jonathan Castello ORCID logo, Patrick Redmond ORCID logo, and Lindsey Kuper ORCID logo
(University of California at Santa Cruz, Santa Cruz, USA)
Info
Quarl: A Learning-Based Quantum Circuit Optimizer
Zikun Li ORCID logo, Jinjun Peng ORCID logo, Yixuan Mei ORCID logo, Sina Lin ORCID logo, Yi Wu ORCID logo, Oded Padon ORCID logo, and Zhihao Jia ORCID logo
(Carnegie Mellon University, USA; Columbia University, USA; Microsoft, USA; Tsinghua University, China; VMware Research, USA)
Published Artifact Artifacts Available
Qualifying System F<:: Some Terms and Conditions May Apply
Edward Lee ORCID logo, Yaoyu Zhao ORCID logo, Ondřej Lhoták ORCID logo, James You ORCID logo, Kavin Satheeskumar ORCID logo, and Jonathan Immanuel Brachthäuser ORCID logo
(University of Waterloo, Canada; EPFL, Lausanne, Switzerland; University of Tübingen, Tübingen, Germany)
Published Artifact Archive submitted (290 kB) Artifacts Available Artifacts Reusable Results Reproduced
Forge: A Tool and Language for Teaching Formal Methods
Tim Nelson ORCID logo, Ben Greenman ORCID logo, Siddhartha Prasad ORCID logo, Tristan Dyer ORCID logo, Ethan Bove ORCID logo, Qianfan Chen ORCID logo, Charles Cutting ORCID logo, Thomas Del Vecchio ORCID logo, Sidney LeVine ORCID logo, Julianne Rudner ORCID logo, Ben Ryjikov ORCID logo, Alexander Varga ORCID logo, Andrew Wagner ORCID logo, Luke West ORCID logo, and Shriram Krishnamurthi ORCID logo
(Brown University, USA; University of Utah, USA; Stashpad, USA; Northeastern University, USA)
Published Artifact Artifacts Available Artifacts Reusable
Design and Implementation of an Aspect-Oriented C Programming Language
Zhe Chen ORCID logo, Yunlong Zhu ORCID logo, and Zhemin Wang ORCID logo
(Nanjing University of Aeronautics and Astronautics, China)
Published Artifact Artifacts Available Artifacts Reusable Results Reproduced
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization
Joseph W. Cutler ORCID logo, Craig Disselkoen ORCID logo, Aaron Eline ORCID logo, Shaobo He ORCID logo, Kyle Headley ORCID logo, Michael Hicks ORCID logo, Kesha Hietala ORCID logo, Eleftherios Ioannidis ORCID logo, John Kastner ORCID logo, Anwar Mamat ORCID logo, Darin McAdams ORCID logo, Matt McCutchen ORCID logo, Neha Rungta ORCID logo, Emina Torlak ORCID logo, and Andrew M. Wells ORCID logo
(University of Pennsylvania, USA; Amazon Web Services, USA; Unaffiliated, USA; University of Maryland, USA)
Artifacts Reusable Results Reproduced
Persimmon: Nested Family Polymorphism with Extensible Variant Types
Anastasiya Kravchuk-Kirilyuk ORCID logo, Gary Feng ORCID logo, Jonas Iskander ORCID logo, Yizhou ZhangORCID logo, and Nada Amin ORCID logo
(Harvard University, USA; University of Waterloo, Canada)
Published Artifact Archive submitted (2.4 MB) Artifacts Available Artifacts Reusable Results Reproduced
Hydra: Generalizing Peephole Optimizations with Program Synthesis
Manasij Mukherjee ORCID logo and John Regehr ORCID logo
(University of Utah, USA)
Multiverse Notebook: Shifting Data Scientists to Time Travelers
Shigeyuki Sato ORCID logo and Tomoki NakamaruORCID logo
(University of Electro-Communications, Japan; University of Tokyo, Japan)
Info Artifacts Functional Results Reproduced
Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs
Martin Avanzini ORCID logo, Gilles Barthe ORCID logo, Benjamin Grégoire ORCID logo, Georg Moser ORCID logo, and Gabriele VanoniORCID logo
(Centre Inria d’Université Côte d’Azur, France; MPI-SP, Germany; IMDEA Software Institute, Spain; University of Innsbruck, Austria)
Published Artifact Artifacts Available Artifacts Reusable Results Reproduced
Accurate Data Race Prediction in the Linux Kernel through Sparse Fourier Learning
Gabriel Ryan ORCID logo, Burcu Cetin ORCID logo, Yongwhan Lim ORCID logo, and Suman JanaORCID logo
(Columbia University, USA)
Published Artifact Artifacts Available Artifacts Functional Results Reproduced
TorchQL: A Programming Framework for Integrity Constraints in Machine Learning
Aaditya NaikORCID logo, Adam Stein ORCID logo, Yinjun Wu ORCID logo, Mayur Naik ORCID logo, and Eric Wong ORCID logo
(University of Pennsylvania, USA)
Published Artifact Archive submitted (1.1 MB) Artifacts Available
Gradually Typed Languages Should Be Vigilant!
Olek Gierczak ORCID logo, Lucy Menon ORCID logo, Christos Dimoulas ORCID logo, and Amal AhmedORCID logo
(Northeastern University, USA; Northwestern University, USA)
Archive submitted (830 kB) Info
Distributions for Compositionally Differentiating Parametric Discontinuities
Jesse Michel ORCID logo, Kevin Mu ORCID logo, Xuanda Yang ORCID logo, Sai Praveen Bangaru ORCID logo, Elias Rojas Collins ORCID logo, Gilbert Bernstein ORCID logo, Jonathan Ragan-Kelley ORCID logo, Michael CarbinORCID logo, and Tzu-Mao Li ORCID logo
(Massachusetts Institute of Technology, USA; University of Washington, USA; University of California at San Diego, San Diego, USA)
Archive submitted (620 kB)
Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
Lutz Klinkenberg ORCID logo, Christian Blumenthal ORCID logo, Mingshuai Chen ORCID logo, Darion Haase ORCID logo, and Joost-Pieter Katoen ORCID logo
(RWTH Aachen University, Aachen, Germany; Zhejiang University, China)
Published Artifact Artifacts Available Artifacts Reusable Results Reproduced
Learning Abstraction Selection for Bayesian Program Analysis
Yifan Zhang ORCID logo, Yuanfeng Shi ORCID logo, and Xin Zhang ORCID logo
(Peking University, China)
Published Artifact Artifacts Available Artifacts Reusable Results Reproduced
Deriving Dependently-Typed OOP from First Principles
David BinderORCID logo, Ingo Skupin ORCID logo, Tim Süberkrüb ORCID logo, and Klaus Ostermann ORCID logo
(University of Tübingen, Tübingen, Germany; Aleph Alpha, Germany)
Published Artifact Archive submitted (110 kB) Info Artifacts Available Artifacts Reusable Results Reproduced
Verification of Neural Networks’ Global Robustness
Anan Kabaha ORCID logo and Dana Drachsler Cohen ORCID logo
(Technion, Israel)
Functional Ownership through Fractional Uniqueness
Daniel Marshall ORCID logo and Dominic Orchard ORCID logo
(University of Kent, United Kingdom; University of Cambridge, United Kingdom)
Published Artifact Artifacts Available Artifacts Reusable Results Reproduced
VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints
Yang He ORCID logo, Pinhan Zhao ORCID logo, Xinyu Wang ORCID logo, and Yuepeng Wang ORCID logo
(Simon Fraser University, Canada; University of Michigan, USA)
Published Artifact Artifacts Available Artifacts Functional
PyDex: Repairing Bugs in Introductory Python Assignments using LLMs
Jialu Zhang ORCID logo, José Pablo Cambronero ORCID logo, Sumit GulwaniORCID logo, Vu LeORCID logo, Ruzica Piskac ORCID logo, Gustavo Soares ORCID logo, and Gust Verbruggen ORCID logo
(University of Waterloo, Canada; Microsoft, USA; Yale University, USA; Microsoft, Belgium)
Seneca: Taint-Based Call Graph Construction for Java Object Deserialization
Joanna C. S. Santos ORCID logo, Mehdi Mirakhorli ORCID logo, and Ali Shokri ORCID logo
(University of Notre Dame, USA; University of Hawaii, Manoa, USA; Virginia Tech, USA)
A Pure Demand Operational Semantics with Applications to Program Analysis
Scott SmithORCID logo and Robert ZhangORCID logo
(Johns Hopkins University, USA)
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 ORCID logo, Aleksander Boruch-Gruszecki ORCID logo, and Martin Odersky ORCID logo
(EPFL, Lausanne, Switzerland)
Archive submitted (1.7 MB)
ParDiff: Practical Static Differential Analysis of Network Protocol Parsers
Mingwei Zheng ORCID logo, Qingkai Shi ORCID logo, Xuwei Liu ORCID logo, Xiangzhe Xu ORCID logo, Le Yu ORCID logo, Congyu LiuORCID logo, Guannan Wei ORCID logo, and Xiangyu ZhangORCID logo
(Purdue University, USA)
A Constraint Solving Approach to Parikh Images of Regular Languages
Amanda StjernaORCID logo and Philipp RümmerORCID logo
(Uppsala University, Uppsala, Sweden; University of Regensburg, Regensburg, Germany)
Published Artifact Artifacts Available Artifacts Functional Results Reproduced
PP-CSA: Practical Privacy-Preserving Software Call Stack Analysis
Zhaoyu Wang ORCID logo, Pingchuan Ma ORCID logo, Huaijin Wang ORCID logo, and Shuai Wang ORCID logo
(Hong Kong University of Science and Technology, China)
Scenario-Based Proofs for Concurrent Objects
Constantin Enea ORCID logo and Eric Koskinen ORCID logo
(LIX - CNRS - École Polytechnique, France; Stevens Institute of Technology, USA)
Published Artifact Artifacts Available Artifacts Functional Results Reproduced
Mechanizing the CMP Abstraction for Parameterized Verification
Yongjian Li ORCID logo, Bohua Zhan ORCID logo, and Jun PangORCID logo
(Institute of Software at Chinese Academy of Sciences, China; University of Luxembourg, Luxembourg)
Artifacts Functional Results Reproduced
Message-Observing Sessions
Ryan KavanaghORCID logo and Brigitte PientkaORCID logo
(Université du Québec à Montréal, Canada; McGill University, Canada)
Understanding and Finding Java Decompiler Bugs
Yifei Lu ORCID logo, Weidong Hou ORCID logo, Minxue PanORCID logo, Xuandong Li ORCID logo, and Zhendong Su ORCID logo
(Nanjing University, China; ETH Zurich, Switzerland)
Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation
Qianchuan Ye ORCID logo and Benjamin DelawareORCID logo
(Purdue University, USA)
Published Artifact Archive submitted (540 kB) Artifacts Available Artifacts Reusable Results Reproduced
Iterative-Epoch Online Cycle Elimination for Context-Free Language Reachability
Pei Xu ORCID logo, Yuxiang Lei ORCID logo, Yulei Sui ORCID logo, and Jingling Xue ORCID logo
(University of Technology Sydney, Australia; UNSW, Sydney, Australia)
Modeling Dynamic (De)Allocations of Local Memory for Translation Validation
Abhishek Rose ORCID logo and Sorav Bansal ORCID logo
(IIT Delhi, India)
Published Artifact Artifacts Available Artifacts Functional

proc time: 14.39