OOPSLA2 2023
Proceedings of the ACM on Programming Languages, Volume 7, Number OOPSLA2

Title Page

Editorial Message

Hardware-Aware Static Optimization of Hyperdimensional Computations
Pu (Luke) Yi and Sara Achour
(Stanford University, USA)

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

Leaf: Modularity for Temporary Sharing in Separation Logic
Travis Hance, Jon Howell, Oded Padon, and Bryan Parno
(Carnegie Mellon University, USA; VMware Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Formally Verifying Optimizations with Block Simulations
Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, and Alexandre Bérard
(Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, France)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Synthesizing Efficient Memoization Algorithms
Yican Sun, Xuanyu Peng, and Yingfei Xiong
(Peking University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

AtomiS: Data-Centric Synchronization Made Practical
Hervé Paulino, Ana Almeida Matos, Jan Cederquist, Marco Giunti, João Matos, and António Ravara
(Nova University of Lisbon, Portugal; University of Lisbon, Portugal)

Publisher's Version

Secure RDTs: Enforcing Access Control Policies for Offline Available JSON Data
Thierry Renaux, Sam Van den Vonder, and Wolfgang De Meuter
(Vrije Universiteit Brussel, Belgium)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Beacons: An End-to-End Compiler Framework for Predicting and Utilizing Dynamic Loop Characteristics
Girish Mururu, Sharjeel Khan, Bodhisatwa Chatterjee, Chao Chen, Chris Porter, Ada Gavrilovska, and Santosh Pande
(Georgia Institute of Technology, USA; IBM Research, USA)

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

Compiling Structured Tensor Algebra
Mahdi Ghorbani, Mathieu Huot, Shideh Hashemian, and Amir Shaikhha
(University of Edinburgh, UK; University of Oxford, UK)

Publisher's Version Artifacts Functional

The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog
Qinlin Chen, Nairen Zhang, Jinpeng Wang, Tian Tan, Chang Xu, Xiaoxing Ma, and Yue Li
(Nanjing University, China)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Run-Time Prevention of Software Integration Failures of Machine Learning APIs
Chengcheng Wan, Yuhan Liu, Kuntai Du, Henry Hoffmann, Junchen Jiang, Michael Maire, and Shan Lu
(East China Normal University, China; University of Chicago, USA; Microsoft, Redmon, USA)

Publisher's Version

The Bounded Pathwidth of Control-Flow Graphs
Giovanna Kobus Conrado, Amir Kafshdar Goharshady, and Chun Kit Lam
(Hong Kong University of Science and Technology, Hong Kong)

Publisher's Version Published Artifact Artifacts Available

AST vs. Bytecode: Interpreters in the Age of Meta-Compilation
Octave Larose, Sophie Kaleba, Humphrey Burchell, and Stefan Marr
(University of Kent, UK)

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

Mutually Iso-Recursive Subtyping
Andreas Rossberg
(Independent Researcher, Munich, Germany)

Publisher's Version

Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity
Chuta Sano, Ryan Kavanagh, and Brigitte Pientka
(McGill University, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies
Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf
(Purdue University, USA; Galois, USA; Augusta University, USA)

Publisher's Version

Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference
Ishan Bhanuka, Lionel Parreaux, David Binder, and Jonathan Immanuel Brachthäuser
(Hong Kong University of Science and Technology, China; University of Tübingen, Germany)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Continuing WebAssembly with Effect Handlers
Luna Phipps-Costin, Andreas Rossberg, Arjun Guha, Daan Leijen, Daniel Hillerström, KC Sivaramakrishnan, Matija Pretnar, and Sam Lindley
(Northeastern University, USA; Independent, Germany; Roblox, USA; Microsoft Research, USA; Huawei Zurich Research Center, Switzerland; Tarides, India; IIT Madras, India; University of Ljubljana, Slovenia; Institute of Mathematics, Physics, and Mechanics, Ljubljana, Slovenia; University of Edinburgh, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Two Birds with One Stone: Boosting Code Generation and Code Search via a Generative Adversarial Network
Shangwen Wang, Bo Lin, Zhensu Sun, Ming Wen, Yepang Liu, Yan Lei, and Xiaoguang Mao
(National University of Defense Technology, China; Singapore Management University, Singapore; Huazhong University of Science and Technology, China; Southern University of Science and Technology, China; Chongqing University, China)

Publisher's Version Published Artifact Artifacts Available

Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems
Magnus Madsen, Jaco van de Pol, and Troels Henriksen
(Aarhus University, Denmark; University of Copenhagen, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

How Profilers Can Help Navigate Type Migration
Ben Greenman, Matthias Felleisen, and Christos Dimoulas
(University of Utah, USA; Northeastern University, USA; Northwestern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Rhombus: A New Spin on Macros without All the Parentheses
Matthew Flatt, Taylor Allred, Nia Angle, Stephen De Gabrielle, Robert Bruce Findler, Jack Firth, Kiran Gopinathan, Ben Greenman, Siddhartha Kasivajhula, Alex Knauth, Jay McCarthy, Sam Phillips, Sorawee Porncharoenwase, Jens Axel Søgaard, and Sam Tobin-Hochstadt
(University of Utah, USA; independent, USA; independent, UK; Northwestern University, USA; National University of Singapore, Singapore; Brown University, USA; Reach, USA; University of Washington, USA; independent, Denmark; Indiana University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Towards Better Semantics Exploration for Browser Fuzzing
Chijin Zhou, Quan Zhang, Lihua Guo, Mingzhe Wang, Yu Jiang, Qing Liao, Zhiyong Wu, Shanshan Li, and Bin Gu
(Tsinghua University, China; Harbin Institute of Technology, China; National University of Defense Technology, China; Beijing Institute of Control Engineering, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory
Simon Friis Vindum and Lars Birkedal
(Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Adventure of a Lifetime: Extract Method Refactoring for Rust
Sewen Thy, Andreea Costea, Kiran Gopinathan, and Ilya Sergey
(Yale-NUS College, Singapore; National University of Singapore, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Mat2Stencil: A Modular Matrix-Based DSL for Explicit and Implicit Matrix-Free PDE Solvers on Structured Grid
Huanqi Cao, Shizhi Tang, Qianchao Zhu, Bowen Yu, and Wenguang Chen
(Tsinghua University, China; Peking University, China; Pengcheng Laboratory, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, and Derek Dreyer
(Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, France; Saarland University, Germany; MPI-SWS, Germany; Aarhus University, Denmark)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable

Interactive Debugging of Datalog Programs
André Pacak and Sebastian Erdweg
(JGU Mainz, Germany)

Publisher's Version

Concrete Type Inference for Code Optimization using Machine Learning with SMT Solving
Fangke Ye, Jisheng Zhao, Jun Shirako, and Vivek Sarkar
(Georgia Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available

An Explanation Method for Models of Code
Yu Wang, Ke Wang, and Linzhang Wang
(Nanjing University, China; Visa Research, USA)

Publisher's Version Archive submitted (570 kB)

Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic
Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Sunho Park, and Jeehoon Kang
(KAIST, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Simple Reference Immutability for System F_<:
Edward Lee and Ondřej Lhoták
(University of Waterloo, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart Contracts
Zhuo Cai, Soroush Farokhnia, Amir Kafshdar Goharshady, and S. Hitarth
(Hong Kong University of Science and Technology, Hong Kong)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Inductive Program Synthesis Guided by Observational Program Similarity
Jack Feser, Işıl Dillig, and Armando Solar-Lezama
(Massachusetts Institute of Technology, USA; University of Texas at Austin, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers
Marius Müller, Philipp Schuster, Jonathan Lindegaard Starup, Klaus Ostermann, and Jonathan Immanuel Brachthäuser
(University of Tübingen, Germany; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

A Container-Usage-Pattern-Based Context Debloating Approach for Object-Sensitive Pointer Analysis
Dongjie He, Yujiang Gui, Wei Li, Yonggang Tao, Changwei Zou, Yulei Sui, and Jingling Xue
(UNSW, Australia)

Publisher's Version

A Cocktail Approach to Practical Call Graph Construction
Yuandao Cai and Charles Zhang
(Hong Kong University of Science and Technology, China)

Publisher's Version

Equality Saturation Theory Exploration à la Carte
Anjali Pal, Brett Saiki, Ryan Tjoa, Cynthia Richey, Amy Zhu, Oliver Flatt, Max Willsey, Zachary Tatlock, and Chandrakana Nandi
(University of Washington, USA; Certora, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Complete First-Order Reasoning for Properties of Functional Programs
Adithya Murali, Lucas Peña, Ranjit Jhala, and P. Madhusudan
(University of Illinois at Urbana-Champaign, USA; University of California at San Diego, USA)

Publisher's Version

Structural Subtyping as Parametric Polymorphism
Wenhao Tang, Daniel Hillerström, James McKinna, Michel Steuwer, Ornela Dardha, Rongxiao Fu, and Sam Lindley
(University of Edinburgh, UK; Huawei Zurich Research Center, Switzerland; Heriot-Watt University, UK; TU Berlin, Germany; University of Glasgow, UK)

Publisher's Version Archive submitted (1.1 MB)

A Pretty Expressive Printer
Sorawee Porncharoenwase, Justin Pombrio, and Emina Torlak
(University of Washington, USA; Unaffiliated, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Automated Ambiguity Detection in Layout-Sensitive Grammars
Jiangyi Liu, Fengmin Zhu, and Fei He
(Tsinghua University, China; CISPA Helmholtz Center for Information Security, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Reusing Just-in-Time Compiled Code
Meetesh Kalpesh Mehta, Sebastián Krynski, Hugo Musso Gualandi, Manas Thakur, and Jan Vitek
(IIT Mandi, India; Czech Technical University in Prague, Czechia; IIT Bombay, India; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Bring Your Own Data Structures to Datalog
Arash Sahebolamri, Langston Barrett, Scott Moore, and Kristopher Micinski
(Syracuse University, USA; Galois, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

A Grounded Conceptual Model for Ownership Types in Rust
Will Crichton, Gavin Gray, and Shriram Krishnamurthi
(Brown University, USA; ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Building Dynamic System Call Sandbox with Partial Order Analysis
Quan Zhang, Chijin Zhou, Yiwen Xu, Zijing Yin, Mingzhe Wang, Zhuo Su, Chengnian Sun, Yu Jiang, and Jiaguang Sun
(Tsinghua University, China; University of Waterloo, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Resource-Aware Soundness for Big-Step Semantics
Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca
(University of Genoa, Italy; University of Eastern Piedmont, Italy)

Publisher's Version

Initializing Global Objects: Time and Order
Fengyun Liu, Ondřej Lhoták, David Hua, and Enze Xing
(Oracle Labs, Switzerland; University of Waterloo, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Formal Abstractions for Packet Scheduling
Anshuman Mohan, Yunhe Liu, Nate Foster, Tobias Kappé, and Dexter Kozen
(Cornell University, USA; Open University of the Netherlands, Netherlands; University of Amsterdam, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Reference Capabilities for Flexible Memory Management
Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, James Noble, Matthew J. Parkinson, and Tobias Wrigstad
(Uppsala University, Sweden; Microsoft Azure Research, USA; Imperial College London, UK; Research & Programming, New Zealand; Microsoft Azure Research, UK)

Publisher's Version

Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates
Aalok Thakkar, Nathaniel Sands, George Petrou, Rajeev Alur, Mayur Naik, and Mukund Raghothaman
(University of Pennsylvania, USA; University of Southern California, USA)

Publisher's Version

MemPerf: Profiling Allocator-Induced Performance Slowdowns
Jin Zhou, Sam Silvestro, Steven (Jiaxun) Tang, Hanmei Yang, Hongyu Liu, Guangming Zeng, Bo Wu, Cong Liu, and Tongping Liu
(University of Massachusetts at Amherst, USA; University of Texas at San Antonio, USA; Synopsys, USA; Colorado School of Mines, USA; University of Texas at Dallas, USA)

Publisher's Version

Verifying Indistinguishability of Privacy-Preserving Protocols
Kirby Linvill, Gowtham Kaki, and Eric Wustrow
(University of Colorado Boulder, USA)

Publisher's Version

Quantifying and Mitigating Cache Side Channel Leakage with Differential Set
Cong Ma, Dinghao Wu, Gang Tan, Mahmut Taylan Kandemir, and Danfeng Zhang
(University of Waterloo, Canada; Pennsylvania State University, USA; Duke University, USA)

Publisher's Version Published Artifact Artifacts Available

How Domain Experts Use an Embedded DSL
Lisa Rennels and Sarah E. Chasins
(University of California at Berkeley, USA)

Publisher's Version

When Concurrency Matters: Behaviour-Oriented Concurrency
Luke Cheeseman, Matthew J. Parkinson, Sylvan Clebsch, Marios Kogias, Sophia Drossopoulou, David Chisnall, Tobias Wrigstad, and Paul Liétar
(Imperial College London, UK; Microsoft Azure Research, UK; Microsoft Research, UK; Microsoft, UK; Uppsala University, Sweden)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

TASTyTruffle: Just-in-Time Specialization of Parametric Polymorphism
Matt D'Souza, James You, Ondřej Lhoták, and Aleksandar Prokopec
(University of Waterloo, Canada; Oracle Labs, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Validating IoT Devices with Rate-Based Session Types
Grant Iraci, Cheng-En Chuang, Raymond Hu, and Lukasz Ziarek
(University at Buffalo, USA; Queen Mary University of London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Static Analysis of Memory Models for SMT Encodings
Thomas Haas, René Maseli, Roland Meyer, and Hernán Ponce de León
(TU Braunschweig, Germany; Huawei, Germany)

Publisher's Version Published Artifact Archive submitted (530 kB) Artifacts Available Artifacts Functional

Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Programs
Alex Renda, Yi Ding, and Michael Carbin
(Massachusetts Institute of Technology, USA; Purdue University, USA)

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

Stuttering for Free
Minki Cho, Youngju Song, Dongjae Lee, Lennard Gäher, and Derek Dreyer
(Seoul National University, Republic of Korea; MPI-SWS, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Inference of Resource Management Specifications
Narges Shadab, Pritam Gharat, Shrey Tiwari, Michael D. Ernst, Martin Kellogg, Shuvendu K. Lahiri, Akash Lal, and Manu Sridharan
(University of California at Riverside, USA; Microsoft Research, India; University of Washington, USA; New Jersey Institute of Technology, USA; Microsoft Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Rapid: Region-Based Pointer Disambiguation
Khushboo Chitre, Piyus Kedia, and Rahul Purandare
(IIIT Delhi, India; University of Nebraska-Lincoln, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Gradual Typing for Effect Handlers
Max S. New, Eric Giovannini, and Daniel R. Licata
(University of Michigan, USA; Wesleyan University, USA)

Publisher's Version

Synthesizing Specifications
Kanghee Park, Loris D'Antoni, and Thomas Reps
(University of Wisconsin-Madison, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks
Pengfei Gao, Yedi Zhang, Fu Song, Taolue Chen, and Francois-Xavier Standaert
(ShanghaiTech University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; University of London, UK; Université Catholique de Louvain, Belgium)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional

Data Extraction via Semantic Regular Expression Synthesis
Qiaochu Chen, Arko Banerjee, Çağatay Demiralp, Greg Durrett, and Işıl Dillig
(University of Texas at Austin, USA; Massachusetts Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols
Orr Tamir, Marcelo Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta, and Mooly Sagiv
(Tel Aviv University, Israel; University of Texas at Austin, USA; VMware Research, USA; VMware Research, Israel)

Publisher's Version

Historia: Refuting Callback Reachability with Message-History Logics
Shawn Meier, Sergio Mover, Gowtham Kaki, and Bor-Yuh Evan Chang
(University of Colorado Boulder, USA; École Polytechnique - CNRS - Institut Polytechnique de Paris, France; Amazon, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

P4R-Type: A Verified API for P4 Control Plane Programs
Jens Kanstrup Larsen, Roberto Guanciale, Philipp Haller, and Alceste Scalas
(DTU, Denmark; KTH Royal Institute of Technology, Sweden)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Synthesizing Precise Static Analyzers for Automatic Differentiation
Jacob Laurel, Siyuan Brant Qian, Gagandeep Singh, and Sasa Misailovic
(University of Illinois at Urbana-Champaign, USA; Zhejiang University, China; VMware Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Exploiting the Sparseness of Control-Flow and Call Graphs for Efficient and On-Demand Algebraic Program Analysis
Giovanna Kobus Conrado, Amir Kafshdar Goharshady, Kerim Kochekov, Yun Chen Tsai, and Ahmed Khaled Zaher
(Hong Kong University of Science and Technology, Hong Kong)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Saggitarius: A DSL for Specifying Grammatical Domains
Anders Miltner, Devon Loehr, Arnold Mong, Kathleen Fisher, and David Walker
(Simon Fraser University, Canada; Princeton University, USA; Tufts University, USA)

Publisher's Version

A Deductive Verification Infrastructure for Probabilistic Programs
Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja
(RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK; DTU, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Greedy Implicit Bounded Quantification
Chen Cui, Shengyi Jiang, and Bruno C. d. S. Oliveira
(University of Hong Kong, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Solving String Constraints with Lengths by Stabilization
Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, and Juraj Síč
(Academia Sinica, Taiwan; Brno University of Technology, Czechia)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Type-Safe Dynamic Placement with First-Class Placed Values
George Zakhour, Pascal Weisenburger, and Guido Salvaneschi
(University of St. Gallen, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Explainable Program Synthesis by Localizing Specifications
Amirmohammad Nazari, Yifei Huang, Roopsha Samanta, Arjun Radhakrishna, and Mukund Raghothaman
(University of Southern California, USA; Purdue University, USA; Microsoft, USA)

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

Perception Contracts for Safety of ML-Enabled Systems
Angello Astorga, Chiao Hsieh, P. Madhusudan, and Sayan Mitra
(University of Illinois at Urbana-Champaign, USA)

Publisher's Version

Message Chains for Distributed System Verification
Federico Mora, Ankush Desai, Elizabeth Polgreen, and Sanjit A. Seshia
(University of California at Berkeley, USA; Amazon Web Services, USA; University of Edinburgh, UK)

Publisher's Version