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

Title Page

Editorial Message

AnICA: Analyzing Inconsistencies in Microarchitectural Code Analyzers
Fabian Ritter  and Sebastian Hack 
(Saarland University, Germany)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

First-Class Names for Effect Handlers
Ningning Xie , Youyou Cong , Kazuki Ikemori , and Daan Leijen 
(University of Cambridge, UK; Tokyo Institute of Technology, Japan; Microsoft Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Compositional Virtual Timelines: Verifying Dynamic-Priority Partitions with Algorithmic Temporal Isolation
Mengqi Liu , Zhong Shao , Hao Chen , Man-Ki Yoon , and Jung-Eun Kim 
(Yale University, USA)

Publisher's Version Artifacts Functional

Parsing Randomness
Harrison Goldstein  and Benjamin C. Pierce 
(University of Pennsylvania, USA)

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

CAAT: Consistency as a Theory
Thomas Haas , Roland Meyer , and Hernán Ponce de León 
(TU Braunschweig, Germany; Huawei, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Reasoning about Distributed Reconfigurable Systems
Emma Ahrens , Marius Bozga , Radu Iosif , and Joost-Pieter Katoen 
(RWTH Aachen University, Aachen, Germany; Université Grenoble Alpes, France; CNRS, France; Grenoble INP, France; VERIMAG, France)

Publisher's Version

Compositional Embeddings of Domain-Specific Languages
Yaozhu Sun , Utkarsh Dhandhania , and Bruno C. d. S. Oliveira 
(University of Hong Kong, China)

Publisher's Version Published Artifact Archive submitted (930 kB) Info Artifacts Available Artifacts Reusable

Scalable Linear Invariant Generation with Farkas’ Lemma
Hongming Liu , Hongfei Fu , Zhiyong Yu , Jiaxin Song , and Guoqiang Li 
(Shanghai Jiao Tong University, China)

Publisher's Version Published Artifact Artifacts Available

Can Guided Decomposition Help End-Users Write Larger Block-Based Programs? A Mobile Robot Experiment
Nico Ritschel , Felipe Fronchetti , Reid Holmes , Ronald Garcia , and David C. Shepherd 
(University of British Columbia, Canada; Virginia Commonwealth University, USA)

Publisher's Version Info

Tower: Data Structures in Quantum Superposition
Charles Yuan  and Michael Carbin 
(Massachusetts Institute of Technology, USA)

Publisher's Version Published Artifact Archive submitted (410 kB) Artifacts Available Artifacts Reusable

Proving Hypersafety Compositionally
Emanuele D’Osualdo , Azadeh Farzan , and Derek Dreyer 
(MPI-SWS, Germany; University of Toronto, Canada)

Publisher's Version

Bridging the Semantic Gap between Qualitative and Quantitative Models of Distributed Systems
Si Liu , Jose Meseguer , Peter Csaba Ölveczky , Min Zhang , and David Basin 
(ETH Zurich, Switzerland; University of Illinois at Urbana-Champaign, USA; University of Oslo, Norway; East China Normal University, China)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional

Concurrent Size
Gal Sela  and Erez Petrank 
(Technion, Israel)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Wildcards Need Witness Protection
Kevin Bierhoff 
(Google, USA)

Publisher's Version Info

Overwatch: Learning Patterns in Code Edit Sequences
Yuhao Zhang , Yasharth Bajpai , Priyanshu Gupta , Ameya Ketkar , Miltiadis Allamanis , Titus Barik , Sumit Gulwani , Arjun Radhakrishna , Mohammad Raza , Gustavo Soares , and Ashish Tiwari 
(University of Wisconsin-Madison, USA; Microsoft, India; Uber, USA; Microsoft Research, UK; Microsoft, USA)

Publisher's Version

Incremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers
Aron Zwaan , Hendrik van Antwerpen , and Eelco Visser 
(Delft University of Technology, Netherlands)

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

MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types
Lionel Parreaux  and Chun Yin Chau 
(Hong Kong University of Science and Technology, China)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional

Highly Illogical, Kirk: Spotting Type Mismatches in the Large Despite Broken Contracts, Unsound Types, and Too Many Linters
Joshua Hoeflich , Robert Bruce Findler , and Manuel Serrano 
(Northwestern University, USA; Inria, France; University of Côte d'Azur, France)

Publisher's Version

Data-Driven Lemma Synthesis for Interactive Proofs
Aishwarya Sivaraman , Alex Sanchez-Stern , Bretton Chen , Sorin Lerner , and Todd Millstein 
(University of California at Los Angeles, USA; University of Massachusetts at Amherst, USA; University of California at San Diego, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Type-Directed Synthesis of Visualizations from Natural Language Queries
Qiaochu Chen , Shankara Pailoor , Celeste Barnaby , Abby Criswell , Chenglong Wang , Greg Durrett , and Işil Dillig 
(University of Texas at Austin, USA; Microsoft Research, USA)

Publisher's Version

Synthesis-Powered Optimization of Smart Contracts via Data Type Refactoring
Yanju Chen , Yuepeng Wang , Maruth Goyal , James Dong , Yu Feng , and Işil Dillig 
(University of California at Santa Barbara, USA; Simon Fraser University, Canada; University of Texas at Austin, USA; Stanford University, USA)

Publisher's Version

Verified Compilation of Quantum Oracles
Liyi Li , Finn Voichick , Kesha Hietala , Yuxiang Peng , Xiaodi Wu , and Michael Hicks 
(University of Maryland, USA; Amazon, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Specification-Guided Component-Based Synthesis from Effectful Libraries
Ashish Mishra  and Suresh Jagannathan 
(Purdue University, USA)

Publisher's Version Published Artifact Artifacts Available

A Fast In-Place Interpreter for WebAssembly
Ben L. Titzer 
(Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

SigVM: Enabling Event-Driven Execution for Truly Decentralized Smart Contracts
Zihan Zhao , Sidi Mohamed Beillahi , Ryan Song , Yuxi Cai , Andreas Veneris , and Fan Long 
(University of Toronto, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Solo: A Lightweight Static Analysis for Differential Privacy
Chiké Abuah , David Darais , and Joseph P. Near 
(University of Vermont, USA; Galois, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

A Conceptual Framework for Safe Object Initialization: A Principled and Mechanized Soundness Proof of the Celsius Model
Clément Blaudeau  and Fengyun Liu 
(Inria, France; Université de Paris-Cité, France; Oracle Labs, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Model Checking for a Multi-Execution Memory Model
Evgenii Moiseenko , Michalis Kokologiannakis , and Viktor Vafeiadis 
(JetBrains Research, Serbia; MPI-SWS, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

The Road Not Taken: Exploring Alias Analysis Based Optimizations Missed by the Compiler
Khushboo Chitre , Piyus Kedia , and Rahul Purandare 
(IIIT Delhi, India; University of Nebraska-Lincoln, USA)

Publisher's Version Published Artifact Artifacts Available

Necessity Specifications for Robustness
Julian Mackay , Susan Eisenbach , James Noble , and Sophia Drossopoulou 
(Victoria University of Wellington, New Zealand; Imperial College London, UK; Creative Research & Programming, New Zealand; Meta, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
Dan Frumin , Emanuele D’Osualdo , Bas van den Heuvel , and Jorge A. Pérez 
(University of Groningen, Netherlands; MPI-SWS, Germany)

Publisher's Version

Coeffects for Sharing and Mutation
Riccardo Bianchini , Francesco Dagnino , Paola Giannini , Elena Zucca , and Marco Servetto 
(University of Genoa, Italy; University of Eastern Piedmont, Italy; Victoria University of Wellington, New Zealand)

Publisher's Version

The Essence of Online Data Processing
Philip Dexter , Yu David Liu , and Kenneth Chiu 
(SUNY Binghamton, USA)

Publisher's Version Published Artifact Artifacts Available

Consistency-Preserving Propagation for SMT Solving of Concurrent Program Verification
Zhihang Sun , Hongyu Fan , and Fei He 
(Tsinghua University, China)

Publisher's Version

Oracle-Free Repair Synthesis for Floating-Point Programs
Daming Zou , Yuchen Gu , Yuanfeng Shi , MingZhe Wang , Yingfei Xiong , and Zhendong Su 
(ETH Zurich, Switzerland; Peking University, China; Princeton University, USA)

Publisher's Version

Optimal Heap Limits for Reducing Browser Memory Use
Marisa Kirisame , Pranav Shenoy , and Pavel Panchekha 
(University of Utah, USA)

Publisher's Version

A General Construction for Abstract Interpretation of Higher-Order Automatic Differentiation
Jacob Laurel , Rem Yang , Shubham Ugare , Robert Nagel , Gagandeep Singh , and Sasa Misailovic 
(University of Illinois at Urbana-Champaign, USA; VMware Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Scalable Verification of GNN-Based Job Schedulers
Haoze Wu , Clark Barrett , Mahmood Sharif , Nina Narodytska , and Gagandeep Singh 
(Stanford University, USA; Tel Aviv University, Israel; VMware Research, USA; University of Illinois at Urbana-Champaign, USA)

Publisher's Version Published Artifact Info Artifacts Available

Fractional Resources in Unbounded Separation Logic
Thibault Dardinier , Peter Müller , and Alexander J. Summers 
(ETH Zurich, Switzerland; University of British Columbia, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Neurosymbolic Repair for Low-Code Formula Languages
Rohan Bavishi , Harshit Joshi , José Cambronero , Anna Fariha , Sumit Gulwani , Vu Le , Ivan Radiček , and Ashish Tiwari 
(University of California at Berkeley, USA; Microsoft, India; Microsoft, USA; Microsoft, Croatia)

Publisher's Version Archive submitted (350 kB)

A Study of Inline Assembly in Solidity Smart Contracts
Stefanos Chaliasos , Arthur Gervais , and Benjamin Livshits 
(Imperial College London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Neural Architecture Search using Property Guided Synthesis
Charles Jin , Phitchaya Mangpo Phothilimthana , and Sudip Roy 
(Massachusetts Institute of Technology, USA; Google Research, USA; Cohere, USA)

Publisher's Version Archive submitted (1.3 MB)

Seq2Parse: Neurosymbolic Parse Error Repair
Georgios Sakkas , Madeline Endres , Philip J. Guo , Westley Weimer , and Ranjit Jhala 
(University of California at San Diego, USA; University of Michigan, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid
Stephen Ellis , Shuofei Zhu , Nobuko Yoshida , and Linhai Song 
(University of Oxford, UK; Pennsylvania State University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Satisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing
Sujit Kumar Muduli  and Subhajit Roy 
(IIT Kanpur, India)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

UniRec: A Unimodular-Like Framework for Nested Recursions and Loops
Kirshanthan Sundararajah , Charitha Saumya , and Milind Kulkarni 
(Purdue University, USA)

Publisher's Version

Synthesizing Abstract Transformers
Pankaj Kumar Kalita , Sujit Kumar Muduli , Loris D’Antoni , Thomas Reps , and Subhajit Roy 
(IIT Kanpur, India; University of Wisconsin-Madison, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Monadic and Comonadic Aspects of Dependency Analysis
Pritam Choudhury 
(University of Pennsylvania, USA)

Publisher's Version

Katara: Synthesizing CRDTs with Verified Lifting
Shadaj Laddad , Conor Power , Mae Milano , Alvin Cheung , and Joseph M. Hellerstein 
(University of California at Berkeley, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

A Concurrent Program Logic with a Future and History
Roland Meyer , Thomas Wies , and Sebastian Wolff 
(TU Braunschweig, Germany; New York University, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Compilation of Dynamic Sparse Tensor Algebra
Stephen Chou  and Saman Amarasinghe 
(Massachusetts Institute of Technology, USA)

Publisher's Version Artifacts Functional

Indexing the Extended Dyck-CFL Reachability for Context-Sensitive Program Analysis
Qingkai Shi , Yongchao Wang , Peisen Yao , and Charles Zhang 
(Ant Group, China; Hong Kong University of Science and Technology, China)

Publisher's Version

Checking Equivalence in a Non-strict Language
John C. Kolesar , Ruzica Piskac , and William T. Hallahan 
(Yale University, USA; Binghamton University, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional

This Is the Moment for Probabilistic Loops
Marcel Moosbrugger , Miroslav Stankovič , Ezio Bartocci , and Laura Kovács 
(TU Wien, Austria)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

A case for DOT: Theoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning
Aleksander Boruch-Gruszecki , Radosław Waśko , Yichen Xu , and Lionel Parreaux 
(EPFL, Switzerland; University of Warsaw, Poland; Beijing University of Posts and Telecommunications, China; Hong Kong University of Science and Technology, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Taming Transitive Redundancy for Context-Free Language Reachability
Yuxiang Lei , Yulei Sui , Shuo Ding , and Qirun Zhang 
(University of Technology Sydney, Australia; Georgia Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Symbolic Execution for Randomized Programs
Zachary Susag , Sumit Lahiri , Justin Hsu , and Subhajit Roy 
(Cornell University, USA; IIT Kanpur, India)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs
Fengmin Zhu , Michael Sammler , Rodolphe Lepigre , Derek Dreyer , and Deepak Garg 
(MPI-SWS, Germany)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

High-Level Effect Handlers in C++
Dan Ghica , Sam Lindley , Marcos Maroñas Bravo , and Maciej Piróg 
(Huawei, UK; University of Edinburgh, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Semi-symbolic Inference for Efficient Streaming Probabilistic Programming
Eric Atkinson , Charles Yuan , Guillaume Baudart , Louis Mandel , and Michael Carbin 
(Massachusetts Institute of Technology, USA; ENS — PSL University — CNRS — Inria, France; IBM Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Synthesizing Axiomatizations using Logic Learning
Paul Krogmeier , Zhengyao Lin , Adithya Murali , and P. Madhusudan 
(University of Illinois at Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available

Veracity: Declarative Multicore Programming with Commutativity
Adam Chen , Parisa Fathololumi , Eric Koskinen , and Jared Pincus 
(Stevens Institute of Technology, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Synthesizing Code Quality Rules from Examples
Pranav Garg  and Srinivasan H. Sengamedu 
(AWS, USA; Amazon, USA)

Publisher's Version Archive submitted (1.2 MB)

Modular Verification of Op-Based CRDTs in Separation Logic
Abel Nieto , Léon Gondelman , Alban Reynaud , Amin Timany , and Lars Birkedal 
(Aarhus University, Denmark; ENS Lyon, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Implementing and Verifying Release-Acquire Transactional Memory in C11
Sadegh Dalvandi  and Brijesh Dongol 
(University of Surrey, UK)

Publisher's Version Published Artifact Artifacts Available

Fast Shadow Execution for Debugging Numerical Errors using Error Free Transformations
Sangeeta Chowdhary  and Santosh Nagarakatte 
(Rutgers University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints
Adithya Murali , Lucas Peña , Eion Blanchard , Christof Löding , and P. Madhusudan 
(University of Illinois at Urbana-Champaign, USA; RWTH Aachen University, Germany)

Publisher's Version Published Artifact Artifacts Available

Intrinsically-Typed Definitional Interpreters à la Carte
Cas van der Rest , Casper Bach Poulsen , Arjen Rouvoet , Eelco Visser , and Peter Mosses 
(Delft University of Technology, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable