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

Title Page

Editorial Message

Sponsors

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

Archive submitted (1.3 MB) 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)

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)

Published Artifact Info Artifacts Available Artifacts Reusable

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

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)

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)

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)

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)

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)

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)

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)

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)

Artifacts Reusable

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

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

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)

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)

Info 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; University of Edinburgh, UK; Tarides, India; IIT Madras, India; University of Ljubljana, Slovenia)

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)

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)

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)

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)

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)

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)

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)

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)

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)

Info Artifacts Reusable

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

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)

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

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, South Korea)

Artifacts Functional

Simple Reference Immutability for System F-Sub
Edward Lee  and Ondřej Lhoták 
(University of Waterloo, Canada)

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)

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)

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)

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)

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

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)

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)

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)

Archive submitted (1.1 MB)

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

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)

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)

Artifacts Reusable

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

Artifacts Functional

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

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)

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)

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

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)

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)

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)

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)

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

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)

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

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)

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)

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)

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)

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)

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

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)

Artifacts Functional

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

Published Artifact Artifacts Available Artifacts Reusable

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

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

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; University of Chinese Academy of Sciences, China; University of London, UK; Université Catholique de Louvain, Belgium)

Info 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)

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)

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)