OOPSLA 2021
Proceedings of the ACM on Programming Languages, Volume 5, Number OOPSLA

Title Page

Editorial Message

Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed Systems
Wolf Honoré , Jieung Kim , Ji-Yong Shin , and Zhong Shao 
(Yale University, USA; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Making Weak Memory Models Fair
Ori Lahav , Egor Namakonov , Jonas Oberhauser, Anton Podkopaev , and Viktor Vafeiadis 
(Tel Aviv University, Israel; St. Petersburg University, Russia; JetBrains Research, Russia; Huawei, Germany; HSE University, Russia; MPI-SWS, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency
Pengbo Yan  and Toby Murray 
(University of Melbourne, Australia)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Semantic Programming by Example with Pre-trained Models
Gust Verbruggen , Vu Le , and Sumit Gulwani 
(KU Leuven, Belgium; Microsoft, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Promises Are Made to Be Broken: Migrating R to Strict Semantics
Aviral Goel , Jan Ječmen , Sebastián Krynski , Olivier Flückiger , and Jan Vitek 
(Northeastern University, USA; Czech Technical University, Czechia)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Efficient Compilation of Algebraic Effect Handlers
Georgios Karachalias , Filip Koprivec, Matija Pretnar , and Tom Schrijvers 
(Tweag, France; University of Ljubljana, Slovenia; Institute of Mathematics, Physics, and Mechanics, Slovenia; KU Leuven, Belgium)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Safer at Any Speed: Automatic Context-Aware Safety Enhancement for Rust
Natalie Popescu, Ziyang Xu, Sotiris Apostolakis, David I. August , and Amit Levy
(Princeton University, USA; Google, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Synthesizing Contracts Correct Modulo a Test Generator
Angello Astorga , Shambwaditya Saha, Ahmad Dinkins, Felicia Wang, P. Madhusudan , and Tao Xie 
(University of Illinois at Urbana-Champaign, USA; Tufts University, USA; Peking University, China)

Publisher's Version

Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches
Masaomi Yamaguchi , Kazutaka Matsuda , Cristina David , and Meng Wang 
(Tohoku University, Japan; University of Bristol, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

SimTyper: Sound Type Inference for Ruby using Type Equality Prediction
Milod Kazerounian, Jeffrey S. Foster, and Bonan Min
(University of Maryland at College Park, USA; Tufts University, USA; Raytheon BBN Technologies, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

ECROs: Building Global Scale Systems from Sequential Code
Kevin De Porre , Carla Ferreira , Nuno Preguiça , and Elisa Gonzalez Boix 
(Vrije Universiteit Brussel, Belgium; NOVA School of Science and Technology, Portugal)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Label Dependent Lambda Calculus and Gradual Typing
Weili Fu, Fabian Krause, and Peter Thiemann 
(University of Freiburg, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Efficient Automatic Scheduling of Imaging and Vision Pipelines for the GPU
Luke Anderson, Andrew Adams, Karima Ma, Tzu-Mao Li, Tian Jin, and Jonathan Ragan-Kelley 
(Massachusetts Institute of Technology, USA; Adobe, USA; University of California at San Diego, USA)

Publisher's Version

Relational Nullable Types with Boolean Unification
Magnus Madsen  and Jaco van de Pol 
(Aarhus University, Denmark)

Publisher's Version

Solver-Based Gradual Type Migration
Luna Phipps-Costin, Carolyn Jane Anderson , Michael Greenberg , and Arjun Guha 
(University of Massachusetts at Amherst, USA; Wellesley College, USA; Stevens Institute of Technology, USA; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

UDF to SQL Translation through Compositional Lazy Inductive Synthesis
Guoqiang Zhang , Yuanchao Xu , Xipeng Shen , and Işıl Dillig 
(North Carolina State University, USA; University of Texas at Austin, USA)

Publisher's Version

Verifying Concurrent Multicopy Search Structures
Nisarg Patel, Siddharth Krishna, Dennis Shasha, and Thomas Wies 
(New York University, USA; Microsoft Research, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Compiling with Continuations, Correctly
Zoe Paraskevopoulou and Anvay Grover
(Northeastern University, USA; University of Wisconsin-Madison, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Statically Bounded-Memory Delayed Sampling for Probabilistic Streams
Eric Atkinson , Guillaume Baudart , Louis Mandel , Charles Yuan , and Michael Carbin 
(Massachusetts Institute of Technology, USA; Inria, France; ENS, France; PSL University, France; IBM Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Data-Driven Abductive Inference of Library Specifications
Zhe Zhou , Robert Dickerson, Benjamin Delaware , and Suresh Jagannathan 
(Purdue University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Formal Verification of High-Level Synthesis
Yann Herklotz , James D. Pollard , Nadesh Ramanathan , and John Wickerson 
(Imperial College London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Program Analysis via Efficient Symbolic Abstraction
Peisen Yao , Qingkai Shi, Heqing Huang, and Charles Zhang 
(Hong Kong University of Science and Technology, China; Ant Group, China)

Publisher's Version

Rewrite Rule Inference Using Equality Saturation
Chandrakana Nandi , Max Willsey , Amy Zhu , Yisu Remy Wang , Brett Saiki , Adam Anderson, Adriana Schulz , Dan Grossman, and Zachary Tatlock 
(University of Washington, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

The Semantics of Shared Memory in Intel CPU/FPGA Systems
Dan Iorga , Alastair F. Donaldson , Tyler Sorensen , and John Wickerson 
(Imperial College London, UK; University of California at Santa Cruz, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Translating C to Safer Rust
Mehmet Emre , Ryan Schroeder, Kyle Dewey , and Ben Hardekopf 
(University of California at Santa Barbara, USA; California State University at Northridge, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

One Down, 699 to Go: or, Synthesising Compositional Desugarings
Sándor Bartha, James Cheney , and Vaishak Belle 
(University of Edinburgh, UK; Alan Turing Institute, UK)

Publisher's Version Published Artifact Artifacts Available

Well-Typed Programs Can Go Wrong: A Study of Typing-Related Bugs in JVM Compilers
Stefanos Chaliasos, Thodoris Sotiropoulos , Georgios-Petros Drosos, Charalambos Mitropoulos, Dimitris Mitropoulos, and Diomidis Spinellis 
(Athens University of Economics and Business, Greece; Technical University of Crete, Greece; University of Athens, Greece; Delft University of Technology, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

A Multiparty Session Typing Discipline for Fault-Tolerant Event-Driven Distributed Programming
Malte Viering , Raymond Hu , Patrick Eugster , and Lukasz Ziarek 
(TU Darmstadt, Germany; Queen Mary University of London, UK; USI Lugano, Switzerland; Purdue University, USA; University at Buffalo, USA)

Publisher's Version Artifacts Reusable Artifacts Functional

What We Eval in the Shadows: A Large-Scale Study of Eval in R Programs
Aviral Goel , Pierre Donat-Bouillud , Filip Křikava, Christoph M. Kirsch, and Jan Vitek 
(Northeastern University, USA; Czech Technical University, Czechia; University of Salzburg, Austria)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Gradually Structured Data
Stefan Malewski, Michael Greenberg , and Éric Tanter 
(University of Chile, Chile; Stevens Institute of Technology, USA; IMFD, Chile)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Artifacts Functional

Transitioning from Structural to Nominal Code with Efficient Gradual Typing
Fabian Muehlboeck  and Ross Tate 
(IST Austria, Austria; Cornell University, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional

Compilation of Sparse Array Programming Models
Rawn Henry, Olivia Hsu , Rohan Yadav, Stephen Chou , Kunle Olukotun , Saman Amarasinghe , and Fredrik Kjolstad 
(Massachusetts Institute of Technology, USA; Stanford University, USA)

Publisher's Version Info

SpecSafe: Detecting Cache Side Channels in a Speculative World
Robert Brotzman, Danfeng Zhang , Mahmut Taylan Kandemir , and Gang Tan
(Pennsylvania State University, USA)

Publisher's Version

Coarsening Optimization for Differentiable Programming
Xipeng Shen , Guoqiang Zhang , Irene Dea, Samantha Andow, Emilio Arroyo-Fang, Neal Gafter, Johann George, Melissa Grueter, Erik Meijer, Olin Grigsby Shivers, Steffi Stumpos, Alanna Tempest, Christy Warden, and Shannon Yang
(North Carolina State University, USA; Facebook, USA)

Publisher's Version

Specifying and Testing GPU Workgroup Progress Models
Tyler Sorensen , Lucas F. Salvador, Harmit Raval, Hugues Evrard, John Wickerson , Margaret Martonosi, and Alastair F. Donaldson 
(University of California at Santa Cruz, USA; Princeton University, USA; Google, USA; Imperial College London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

MonkeyDB: Effectively Testing Correctness under Weak Isolation Levels
Ranadeep Biswas, Diptanshu Kakwani, Jyothi Vedurada, Constantin Enea, and Akash Lal 
(Informal Systems, France; Microsoft, India; IIT Hyderabad, India; IRIF, France; University of Paris, France; CNRS, France; Microsoft Research, India)

Publisher's Version Published Artifact Artifacts Available

Durable Functions: Semantics for Stateful Serverless
Sebastian Burckhardt, Chris Gillum, David Justo, Konstantinos Kallas , Connor McMahon, and Christopher S. Meiklejohn
(Microsoft Research, USA; Microsoft Azure, USA; University of Pennsylvania, USA; Carnegie Mellon University, USA)

Publisher's Version

Gauss: Program Synthesis by Reasoning over Graphs
Rohan Bavishi , Caroline Lemieux, Koushik Sen, and Ion Stoica
(University of California at Berkeley, USA)

Publisher's Version

A Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs
Paul He , Eddy Westbrook, Brent Carmer, Chris Phifer , Valentin Robert, Karl Smeltzer, Andrei Ştefănescu, Aaron Tomb, Adam Wick, Matthew Yacavone, and Steve Zdancewic 
(University of Pennsylvania, USA; Galois, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Copy-and-Patch Compilation: A Fast Compilation Algorithm for High-Level Languages and Bytecode
Haoran Xu  and Fredrik Kjolstad 
(Stanford University, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Artifacts Functional

Study of the Subtyping Machine of Nominal Subtyping with Variance
Ori Roth 
(Technion, Israel)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Dynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence Relations
Didier Ishimwe , KimHao Nguyen , and ThanhVu Nguyen 
(University of Nebraska-Lincoln, USA; George Mason University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs
Yuyan Bao, Guannan Wei , Oliver Bračevac, Yuxuan Jiang , Qiyang He, and Tiark Rompf 
(University of Waterloo, Canada; Purdue University, USA)

Publisher's Version

Static Detection of Silent Misconfigurations with Deep Interaction Analysis
Jialu Zhang, Ruzica Piskac , Ennan Zhai, and Tianyin Xu 
(Yale University, USA; Alibaba Group, USA; University of Illinois at Urbana-Champaign, USA)

Publisher's Version Artifacts Functional

Interpretable Noninterference Measurement and Its Application to Processor Designs
Ziqiao Zhou and Michael K. Reiter
(Microsoft Research, USA; Duke University, USA)

Publisher's Version Info

Reconciling Optimization with Secure Compilation
Son Tuan Vu, Albert Cohen , Arnaud De Grandmaison, Christophe Guillon, and Karine Heydemann
(Sorbonne University, France; CNRS, France; LIP6, France; Google, France; ARM, France; STMicroelectronics, France)

Publisher's Version

Scalability and Precision by Combining Expressive Type Systems and Deductive Verification
Florian Lanzinger , Alexander Weigl , Mattias Ulbrich , and Werner Dietl 
(KIT, Germany; University of Waterloo, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

VESPA: Static Profiling for Binary Optimization
Angélica Aparecida Moreira , Guilherme Ottoni, and Fernando Magno Quintão Pereira 
(Federal University of Minas Gerais, Brazil; Facebook, USA)

Publisher's Version Published Artifact Artifacts Available

Modular Specification and Verification of Closures in Rust
Fabian Wolff, Aurel Bílý , Christoph Matheja , Peter Müller , and Alexander J. Summers 
(ETH Zurich, Switzerland; University of British Columbia, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Rich Specifications for Ethereum Smart Contract Verification
Christian Bräm, Marco Eilers , Peter Müller , Robin Sierra, and Alexander J. Summers 
(ETH Zurich, Switzerland; University of British Columbia, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Making Pointer Analysis More Precise by Unleashing the Power of Selective Context Sensitivity
Tian Tan , Yue Li , Xiaoxing Ma , Chang Xu , and Yannis Smaragdakis 
(Nanjing University, China; University of Athens, Greece)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

LXM: Better Splittable Pseudorandom Number Generators (and Almost as Fast)
Guy L. Steele Jr.  and Sebastiano Vigna 
(Oracle Labs, USA; University of Milan, Italy)

Publisher's Version

Permchecker: A Toolchain for Debugging Memory Managers with Typestate
Karl Cronburg  and Samuel Z. Guyer
(Tufts University, USA)

Publisher's Version

Type Stability in Julia: Avoiding Performance Pathologies in JIT Compilation
Artem Pelenitsyn , Julia Belyakova , Benjamin Chung , Ross Tate , and Jan Vitek 
(Northeastern University, USA; Cornell University, USA; Czech Technical University, Czechia)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Artifacts Functional

A Derivative-Based Parser Generator for Visibly Pushdown Grammars
Xiaodong Jia , Ashish Kumar , and Gang Tan 
(Pennsylvania State University, USA)

Publisher's Version

Generative Type-Aware Mutation for Testing SMT Solvers
Jiwon Park, Dominik Winterer, Chengyu Zhang , and Zhendong Su 
(École Polytechnique, France; ETH Zurich, Switzerland; East China Normal University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

LooPy: Interactive Program Synthesis with Control Structures
Kasra Ferdowsifard , Shraddha Barke , Hila Peleg , Sorin Lerner , and Nadia Polikarpova 
(University of California at San Diego, USA; Technion, Israel)

Publisher's Version Published Artifact Artifacts Available

Not So Fast: Understanding and Mitigating Negative Impacts of Compiler Optimizations on Code Reuse Gadget Sets
Michael D. Brown , Matthew Pruett, Robert Bigelow, Girish Mururu , and Santosh Pande 
(Georgia Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

How Statically-Typed Functional Programmers Write Code
Justin Lubin  and Sarah E. Chasins 
(University of California at Berkeley, USA)

Publisher's Version

Fully Automated Functional Fuzzing of Android Apps for Detecting Non-crashing Logic Bugs
Ting Su , Yichen Yan, Jue Wang , Jingling Sun , Yiheng Xiong, Geguang Pu , Ke Wang , and Zhendong Su 
(East China Normal University, China; Nanjing University, China; Visa Research, USA; ETH Zurich, Switzerland)

Publisher's Version

QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems
Nouraldin Jaber , Christopher Wagner , Swen Jacobs, Milind Kulkarni , and Roopsha Samanta 
(Purdue University, USA; CISPA, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Multi-modal Program Inference: A Marriage of Pre-trained Language Models and Component-Based Synthesis
Kia Rahmani, Mohammad Raza , Sumit Gulwani , Vu Le , Daniel Morris, Arjun Radhakrishna , Gustavo Soares, and Ashish Tiwari 
(Purdue University, USA; Microsoft, USA)

Publisher's Version

Compacting Points-To Sets through Object Clustering
Mohamad Barbar and Yulei Sui 
(University of Technology Sydney, Australia; CSIRO’s Data61, Australia)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Automatic Migration from Synchronous to Asynchronous JavaScript APIs
Satyajit Gokhale, Alexi Turcotte , and Frank Tip 
(Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

APIfix: Output-Oriented Program Synthesis for Combating Breaking Changes in Libraries
Xiang Gao, Arjun Radhakrishna , Gustavo Soares, Ridwan Shariffdeen , Sumit Gulwani , and Abhik Roychoudhury 
(National University of Singapore, Singapore; Microsoft, USA)

Publisher's Version

FPL: Fast Presburger Arithmetic through Transprecision
Arjun Pitchanathan, Christian Ulmann, Michel Weber, Torsten Hoefler, and Tobias Grosser 
(IIIT Hyderabad, India; ETH Zurich, Switzerland; University of Edinburgh, UK)

Publisher's Version Published Artifact Artifacts Available

Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts
Yannis Smaragdakis, Neville Grech, Sifis Lagouvardos , Konstantinos Triantafyllou, and Ilias Tsatiris 
(University of Athens, Greece; University of Malta, Malta)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

The Reads-From Equivalence for the TSO and PSO Memory Models
Truc Lam Bui, Krishnendu Chatterjee , Tushar Gautam, Andreas Pavlogiannis , and Viktor Toman
(Comenius University Bratislava, Slovakia; IST Austria, Austria; IIT Bombay, India; Aarhus University, Denmark)

Publisher's Version

JavaDL: Automatically Incrementalizing Java Bug Pattern Detection
Alexandru Dura , Christoph Reichenbach , and Emma Söderberg 
(Lund University, Sweden)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional

Programming and Execution Models for Parallel Bounded Exhaustive Testing
Nader Al Awar, Kush Jain, Christopher J. Rossbach , and Milos Gligoric 
(University of Texas at Austin, USA; Katana Graph, USA)

Publisher's Version

Generalizable Synthesis through Unification
Ruyi Ji , Jingtao Xia, Yingfei Xiong , and Zhenjiang Hu 
(Peking University, China)

Publisher's Version Published Artifact Artifacts Available