OOPSLA2 2022
Proceedings of the ACM on Programming Languages, Volume 6, Number OOPSLA2
Powered by
Conference Publishing Consulting

Proceedings of the ACM on Programming Languages, Volume 6, Number OOPSLA2, December 8–10, 2022, Auckland, New Zealand

OOPSLAB – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message
Sponsors

Papers

AnICA: Analyzing Inconsistencies in Microarchitectural Code Analyzers
Fabian RitterORCID logo and Sebastian HackORCID logo
(Saarland University, Germany)
Article Search Info Artifacts Available Artifacts Reusable
First-Class Names for Effect Handlers
Ningning Xie ORCID logo, Youyou Cong ORCID logo, Kazuki Ikemori ORCID logo, and Daan LeijenORCID logo
(University of Cambridge, UK; Tokyo Institute of Technology, Japan; Microsoft Research, USA)
Article Search Artifacts Available Artifacts Reusable
Compositional Virtual Timelines: Verifying Dynamic-Priority Partitions with Algorithmic Temporal Isolation
Mengqi Liu ORCID logo, Zhong Shao ORCID logo, Hao Chen ORCID logo, Man-Ki Yoon ORCID logo, and Jung-Eun Kim ORCID logo
(Yale University, USA)
Article Search Artifacts Functional
Parsing Randomness
Harrison GoldsteinORCID logo and Benjamin C. PierceORCID logo
(University of Pennsylvania, USA)
Article Search Artifacts Available
CAAT: Consistency as a Theory
Thomas Haas ORCID logo, Roland Meyer ORCID logo, and Hernán Ponce de León ORCID logo
(TU Braunschweig, Germany; Huawei, Germany)
Article Search Artifacts Available Artifacts Functional
Reasoning about Distributed Reconfigurable Systems
Emma Ahrens ORCID logo, Marius Bozga ORCID logo, Radu Iosif ORCID logo, and Joost-Pieter Katoen ORCID logo
(RWTH Aachen University, Germany; CNRS, France; Université Grenoble Alpes, France)
Article Search
Compositional Embeddings of Domain-Specific Languages
Yaozhu SunORCID logo, Utkarsh Dhandhania ORCID logo, and Bruno C. d. S. OliveiraORCID logo
(University of Hong Kong, China)
Article Search Archive submitted (930 kB) Info Artifacts Available Artifacts Reusable
Scalable Linear Invariant Generation with Farkas’ Lemma
Hongming Liu ORCID logo, Hongfei Fu ORCID logo, Zhiyong Yu ORCID logo, Jiaxin Song ORCID logo, and Guoqiang Li ORCID logo
(Shanghai Jiao Tong University, China)
Article Search Artifacts Available
Can Guided Decomposition Help End-Users Write Larger Block-Based Programs? A Mobile Robot Experiment
Nico RitschelORCID logo, Felipe FronchettiORCID logo, Reid HolmesORCID logo, Ronald GarciaORCID logo, and David C. ShepherdORCID logo
(University of British Columbia, Canada; Virginia Commonwealth University, USA)
Article Search Info
Tower: Data Structures in Quantum Superposition
Charles Yuan ORCID logo and Michael CarbinORCID logo
(Massachusetts Institute of Technology, USA)
Preprint Archive submitted (410 kB) Artifacts Available Artifacts Reusable
Proving Hypersafety Compositionally
Emanuele D’Osualdo ORCID logo, Azadeh FarzanORCID logo, and Derek DreyerORCID logo
(MPI-SWS, Germany; University of Toronto, Canada)
Preprint
Bridging the Semantic Gap between Qualitative and Quantitative Models of Distributed Systems
Si Liu ORCID logo, Jose Meseguer ORCID logo, Peter Csaba ÖlveczkyORCID logo, Min ZhangORCID logo, and David Basin ORCID logo
(ETH Zurich, Switzerland; University of Illinois at Urbana-Champaign, USA; University of Oslo, Norway; East China Normal University, China)
Article Search Info Artifacts Available Artifacts Functional
Concurrent Size
Gal Sela ORCID logo and Erez Petrank ORCID logo
(Technion, Israel)
Article Search Artifacts Available Artifacts Reusable
Wildcards Need Witness Protection
Kevin Bierhoff ORCID logo
(Google, USA)
Article Search Info
Overwatch: Learning Patterns in Code Edit Sequences
Yuhao Zhang ORCID logo, Yasharth Bajpai ORCID logo, Priyanshu Gupta ORCID logo, Ameya Ketkar ORCID logo, Miltiadis Allamanis ORCID logo, Titus Barik ORCID logo, Sumit GulwaniORCID logo, Arjun Radhakrishna ORCID logo, Mohammad Raza ORCID logo, Gustavo Soares ORCID logo, and Ashish Tiwari ORCID logo
(University of Wisconsin-Madison, USA; Microsoft, n.n.; Microsoft, India; Uber, n.n.; Microsoft Research, UK; Microsoft Research, USA; Microsoft, Canada)
Preprint
Incremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers
Aron Zwaan ORCID logo, Hendrik van Antwerpen ORCID logo, and Eelco Visser ORCID logo
(Delft University of Technology, Netherlands)
Article Search Archive submitted (1.2 MB) Artifacts Available Artifacts Functional
MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types
Lionel Parreaux ORCID logo and Chun Yin Chau ORCID logo
(The Hong Kong University of Science and Technology, China)
Article Search Artifacts Available Artifacts Functional
Highly Illogical, Kirk: Spotting Type Mismatches in the Large Despite Broken Contracts, Unsound Types, and Too Many Linters
Joshua HoeflichORCID logo, Robert Bruce Findler ORCID logo, and Manuel SerranoORCID logo
(Northwestern University, USA; Inria, France; University of Côte d'Azur, France)
Article Search
Data-Driven Lemma Synthesis for Interactive Proofs
Aishwarya Sivaraman ORCID logo, Alex Sanchez-Stern ORCID logo, Bretton Chen ORCID logo, Sorin LernerORCID logo, and Todd Millstein ORCID logo
(University of California at Los Angeles, USA; University of Massachusetts at Amherst, USA; University of California at San Diego, USA)
Article Search Artifacts Available Artifacts Functional
Type-Directed Synthesis of Visualizations from Natural Language Queries
Qiaochu Chen ORCID logo, Shankara Pailoor ORCID logo, Celeste Barnaby ORCID logo, Abby Criswell ORCID logo, Chenglong Wang ORCID logo, Greg Durrett ORCID logo, and Işil Dillig ORCID logo
(University of Texas at Austin, USA; Microsoft Research, n.n.)
Article Search
Synthesis-Powered Optimization of Smart Contracts via Data Type Refactoring
Yanju Chen ORCID logo, Yuepeng Wang ORCID logo, Maruth Goyal ORCID logo, James Dong ORCID logo, Yu FengORCID logo, and Işil Dillig ORCID logo
(University of California at Santa Barbara, USA; Simon Fraser University, Canada; University of Texas at Austin, USA; Stanford University, USA)
Article Search
Verified Compilation of Quantum Oracles
Liyi Li ORCID logo, Finn Voichick ORCID logo, Kesha HietalaORCID logo, Yuxiang Peng ORCID logo, Xiaodi Wu ORCID logo, and Michael HicksORCID logo
(University of Maryland, USA; Amazon, USA)
Article Search Info Artifacts Available Artifacts Reusable
Specification-Guided Component-Based Synthesis from Effectful Libraries
Ashish Mishra ORCID logo and Suresh Jagannathan ORCID logo
(Purdue University, USA)
Article Search Artifacts Available
A Fast In-Place Interpreter for WebAssembly
Ben L. Titzer ORCID logo
(Carnegie Mellon University, USA)
Article Search Artifacts Available Artifacts Reusable
SigVM: Enabling Event-Driven Execution for Truly Decentralized Smart Contracts
Zihan Zhao ORCID logo, Sidi Mohamed Beillahi ORCID logo, Ryan Song ORCID logo, Yuxi Cai ORCID logo, Andreas Veneris ORCID logo, and Fan Long ORCID logo
(University of Toronto, Canada)
Article Search Artifacts Available Artifacts Functional
Solo: A Lightweight Static Analysis for Differential Privacy
Chiké Abuah ORCID logo, David Darais ORCID logo, and Joseph P. Near ORCID logo
(University of Vermont, USA; Galois, USA)
Preprint Info Artifacts Available Artifacts Reusable
A Conceptual Framework for Safe Object Initialization
Clément Blaudeau ORCID logo and Fengyun Liu ORCID logo
(Inria, France; Oracle Labs, Switzerland)
Article Search Artifacts Available Artifacts Reusable
Model Checking for a Multi-Execution Memory Model
Evgenii Moiseenko ORCID logo, Michalis KokologiannakisORCID logo, and Viktor VafeiadisORCID logo
(JetBrains Research, Serbia; MPI-SWS, Germany)
Article Search Artifacts Available Artifacts Reusable
The Road Not Taken: Exploring Alias Analysis Based Optimizations Missed by the Compiler
Khushboo Chitre ORCID logo, Piyus Kedia ORCID logo, and Rahul Purandare ORCID logo
(IIIT Delhi, India)
Article Search Artifacts Available
Necessity Specifications for Robustness
Julian Mackay ORCID logo, Susan Eisenbach ORCID logo, James NobleORCID logo, and Sophia Drossopoulou ORCID logo
(Victoria University of Wellington, New Zealand; Imperial College London, UK; Research & Programming, New Zealand; Facebook, UK)
Article Search Artifacts Available Artifacts Functional
A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
Dan Frumin ORCID logo, Emanuele D’Osualdo ORCID logo, Bas van den Heuvel ORCID logo, and Jorge A. Pérez ORCID logo
(University of Groningen, Netherlands; MPI-SWS, Germany)
Article Search
Coeffects for Sharing and Mutation
Riccardo Bianchini ORCID logo, Francesco Dagnino ORCID logo, Paola Giannini ORCID logo, Elena ZuccaORCID logo, and Marco Servetto ORCID logo
(University of Genoa, Italy; University of Eastern Piedmont, Italy; Victoria University of Wellington, New Zealand)
Article Search
The Essence of Online Data Processing
Philip Dexter ORCID logo, Yu David LiuORCID logo, and Kenneth Chiu ORCID logo
(SUNY Binghamton, USA)
Article Search Artifacts Available
Consistency-Preserving Propagation for SMT Solving of Concurrent Program Verification
Zhihang Sun ORCID logo, Hongyu Fan ORCID logo, and Fei HeORCID logo
(Tsinghua University, China)
Article Search
Oracle-Free Repair Synthesis for Floating-Point Programs
Daming Zou ORCID logo, Yuchen Gu ORCID logo, Yuanfeng Shi ORCID logo, MingZhe Wang ORCID logo, Yingfei Xiong ORCID logo, and Zhendong Su ORCID logo
(ETH Zurich, Switzerland; Peking University, China; Princeton University, USA)
Article Search
Optimal Heap Limits for Reducing Browser Memory Use
Marisa KirisameORCID logo, Pranav Shenoy ORCID logo, and Pavel PanchekhaORCID logo
(University of Utah, USA)
Article Search
A General Construction for Abstract Interpretation of Higher-Order Automatic Differentiation
Jacob Laurel ORCID logo, Rem Yang ORCID logo, Shubham UgareORCID logo, Robert Nagel ORCID logo, Gagandeep SinghORCID logo, and Sasa MisailovicORCID logo
(University of Illinois at Urbana-Champaign, USA)
Article Search Artifacts Available Artifacts Functional
Scalable Verification of GNN-Based Job Schedulers
Haoze Wu ORCID logo, Clark Barrett ORCID logo, Mahmood Sharif ORCID logo, Nina Narodytska ORCID logo, and Gagandeep SinghORCID logo
(Stanford University, USA; Tel Aviv University, Israel; VMware Research, USA; University of Illinois at Urbana-Champaign, USA)
Article Search Info Artifacts Available
Fractional Resources in Unbounded Separation Logic
Thibault DardinierORCID logo, Peter Müller ORCID logo, and Alexander J. Summers ORCID logo
(ETH Zurich, Switzerland; University of British Columbia, Canada)
Article Search Artifacts Available Artifacts Reusable
Neurosymbolic Repair for Low-Code Formula Languages
Rohan Bavishi ORCID logo, Harshit Joshi ORCID logo, José Pablo Cambronero ORCID logo, Anna Fariha ORCID logo, Sumit GulwaniORCID logo, Vu LeORCID logo, Ivan Radiček ORCID logo, and Ashish Tiwari ORCID logo
(University of California at Berkeley, USA; Microsoft, India; Microsoft, USA; Microsoft, Croatia)
Article Search Archive submitted (350 kB)
A Study of Inline Assembly in Solidity Smart Contracts
Stefanos Chaliasos ORCID logo, Arthur Gervais ORCID logo, and Benjamin Livshits ORCID logo
(Imperial College London, UK)
Article Search Artifacts Available Artifacts Reusable
Neural Architecture Search using Property Guided Synthesis
Charles JinORCID logo, Phitchaya Mangpo Phothilimthana ORCID logo, and Sudip Roy ORCID logo
(Massachusetts Institute of Technology, USA; Google Research, USA; Cohere.ai, USA)
Article Search Archive submitted (1.3 MB)
Seq2Parse: Neurosymbolic Parse Error Repair
Georgios SakkasORCID logo, Madeline EndresORCID logo, Philip J. Guo ORCID logo, Westley Weimer ORCID logo, and Ranjit Jhala ORCID logo
(University of California at San Diego, USA; University of Michigan, USA)
Article Search Artifacts Available Artifacts Functional
Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid
Stephen Ellis ORCID logo, Shuofei Zhu ORCID logo, Nobuko Yoshida ORCID logo, and Linhai Song ORCID logo
(Imperial College London, UK; Pennsylvania State University, USA; University of Oxford, UK)
Article Search Artifacts Available Artifacts Functional
Satisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing
Sujit Kumar MuduliORCID logo and Subhajit RoyORCID logo
(IIT Kanpur, India)
Article Search Artifacts Available Artifacts Reusable
UniRec: A Unimodular-Like Framework for Nested Recursions and Loops
Kirshanthan SundararajahORCID logo, Charitha SaumyaORCID logo, and Milind KulkarniORCID logo
(Purdue University, USA)
Article Search
Synthesizing Abstract Transformers
Pankaj Kumar Kalita ORCID logo, Sujit Kumar MuduliORCID logo, Loris D’AntoniORCID logo, Thomas RepsORCID logo, and Subhajit RoyORCID logo
(IIT Kanpur, India; University of Wisconsin-Madison, USA)
Article Search Artifacts Available Artifacts Functional
Monadic and Comonadic Aspects of Dependency Analysis
Pritam Choudhury ORCID logo
(University of Pennsylvania, USA)
Article Search
Katara: Synthesizing CRDTs with Verified Lifting
Shadaj Laddad ORCID logo, Conor Power ORCID logo, Mae Milano ORCID logo, Alvin Cheung ORCID logo, and Joseph M. Hellerstein ORCID logo
(University of California at Berkeley, USA)
Article Search Artifacts Available Artifacts Functional
A Concurrent Program Logic with a Future and History
Roland Meyer ORCID logo, Thomas Wies ORCID logo, and Sebastian Wolff ORCID logo
(TU Braunschweig, Germany; New York University, USA)
Preprint Info Artifacts Available Artifacts Reusable
Compilation of Dynamic Sparse Tensor Algebra
Stephen ChouORCID logo and Saman AmarasingheORCID logo
(Massachusetts Institute of Technology, USA)
Article Search Artifacts Functional
Indexing the Extended Dyck-CFL Reachability for Context-Sensitive Program Analysis
Qingkai ShiORCID logo, Yongchao Wang ORCID logo, Peisen YaoORCID logo, and Charles ZhangORCID logo
(Ant Group, China; Hong Kong University of Science and Technology, China)
Article Search
Checking Equivalence in a Non-strict Language
John C. Kolesar ORCID logo, Ruzica Piskac ORCID logo, and William T. Hallahan ORCID logo
(Yale University, USA)
Article Search Info Artifacts Available Artifacts Functional
This Is the Moment for Probabilistic Loops
Marcel MoosbruggerORCID logo, Miroslav StankovičORCID logo, Ezio BartocciORCID logo, and Laura KovácsORCID logo
(TU Wien, Austria)
Article Search Artifacts Available Artifacts Reusable
A case for DOT: Theoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning
Aleksander Boruch-Gruszecki ORCID logo, Radosław Waśko ORCID logo, Yichen XuORCID logo, and Lionel Parreaux ORCID logo
(EPFL, Switzerland; University of Warsaw, Poland; Beijing University of Posts and Telecommunications, China; Hong Kong University of Science and Technology, China)
Article Search Artifacts Available Artifacts Reusable
Taming Transitive Redundancy for Context-Free Language Reachability
Yuxiang Lei ORCID logo, Yulei SuiORCID logo, Shuo Ding ORCID logo, and Qirun Zhang ORCID logo
(University of Technology Sydney, Australia; Georgia Institute of Technology, USA)
Article Search Artifacts Available Artifacts Reusable
Symbolic Execution for Randomized Programs
Zachary Susag ORCID logo, Sumit LahiriORCID logo, Justin Hsu ORCID logo, and Subhajit RoyORCID logo
(Cornell University, USA; IIT Kanpur, India)
Article Search Artifacts Available Artifacts Functional
BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs
Fengmin ZhuORCID logo, Michael Sammler ORCID logo, Rodolphe Lepigre ORCID logo, Derek DreyerORCID logo, and Deepak GargORCID logo
(MPI-SWS, Germany)
Preprint Info Artifacts Available Artifacts Reusable
High-Level Effect Handlers in C++
Dan Ghica ORCID logo, Sam Lindley ORCID logo, Marcos Maronas Bravo ORCID logo, and Maciej PirógORCID logo
(Huawei, UK; University of Edinburgh, UK)
Article Search Artifacts Available Artifacts Reusable
Semi-symbolic Inference for Efficient Streaming Probabilistic Programming
Eric Atkinson ORCID logo, Charles Yuan ORCID logo, Guillaume BaudartORCID logo, Louis Mandel ORCID logo, and Michael Carbin ORCID logo
(Massachusetts Institute of Technology, USA; Inria, France; IBM Research, USA)
Article Search Artifacts Available Artifacts Reusable
Synthesizing Axiomatizations using Logic Learning
Paul Krogmeier ORCID logo, Zhengyao Lin ORCID logo, Adithya Murali ORCID logo, and P. MadhusudanORCID logo
(University of Illinois at Urbana-Champaign, USA)
Article Search Artifacts Available
Veracity: Declarative Multicore Programming with Commutativity
Adam Chen ORCID logo, Parisa Fathololumi ORCID logo, Eric Koskinen ORCID logo, and Jared Pincus ORCID logo
(Stevens Institute of Technology, USA)
Article Search Info Artifacts Available Artifacts Reusable
Synthesizing Code Quality Rules from Examples
Pranav Garg ORCID logo and Srinivasan H. Sengamedu ORCID logo
(AWS, USA; Amazon, USA)
Article Search Archive submitted (1.2 MB)
Modular Verification of Op-Based CRDTs in Separation Logic
Abel Nieto ORCID logo, Léon Gondelman ORCID logo, Alban Reynaud ORCID logo, Amin TimanyORCID logo, and Lars BirkedalORCID logo
(Aarhus University, Denmark; ENS Lyon, France)
Preprint Artifacts Available Artifacts Reusable
Implementing and Verifying Release-Acquire Transactional Memory in C11
Sadegh Dalvandi ORCID logo and Brijesh Dongol ORCID logo
(University of Surrey, UK)
Article Search Artifacts Available
Fast Shadow Execution for Debugging Numerical Errors using Error Free Transformations
Sangeeta Chowdhary ORCID logo and Santosh Nagarakatte ORCID logo
(Rutgers University, USA)
Article Search Artifacts Available Artifacts Functional
Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints
Adithya Murali ORCID logo, Lucas Peña ORCID logo, Eion Blanchard ORCID logo, Christof Löding ORCID logo, and P. MadhusudanORCID logo
(University of Illinois at Urbana-Champaign, USA; RWTH Aachen University, Germany)
Article Search Artifacts Available
Intrinsically-Typed Definitional Interpreters à la Carte
Cas van der RestORCID logo, Casper Bach Poulsen ORCID logo, Arjen Rouvoet ORCID logo, Eelco Visser ORCID logo, and Peter Mosses ORCID logo
(Delft University of Technology, Netherlands)
Article Search Artifacts Available Artifacts Reusable

proc time: 0.08