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

Title Page

Article: oopslaa23foreword-fm000-p doi:

Editorial Message

Article: oopslaa23foreword-fm001-p doi:

Accelerating Fuzzing through Prefix-Guided Execution
Shaohua Li and Zhendong Su
(ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslaa23main-p11-p doi:10.1145/3586027

Solving Conditional Linear Recurrences for Program Verification: The Periodic Case
Chenglin Wang and Fangzhen Lin
(Hong Kong University of Science and Technology, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslaa23main-p18-p doi:10.1145/3586028

Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier
Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, and Grigore Roşu
(Carnegie Mellon University, USA; University of Illinois at Urbana-Champaign, USA; Advanced Digital Sciences Center, Singapore)

Publisher's Version Published Artifact Archive submitted (1.1 MB) Artifacts Available Artifacts Reusable Article: oopslaa23main-p23-p doi:10.1145/3586029

Grounded Copilot: How Programmers Interact with Code-Generating Models
Shraddha Barke, Michael B. James, and Nadia Polikarpova
(University of California at San Diego, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslaa23main-p24-p doi:10.1145/3586030

Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection
Lorenzo Gheri and Nobuko Yoshida
(University of Oxford, UK)

Publisher's Version Article: oopslaa23main-p25-p doi:10.1145/3586031

Languages with Decidable Learning: A Meta-theorem
Paul Krogmeier and P. Madhusudan
(University of Illinois at Urbana-Champaign, USA)

Publisher's Version Article: oopslaa23main-p28-p doi:10.1145/3586032

Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems via Bounded Regions
Christopher Wagner, Nouraldin Jaber, and Roopsha Samanta
(Purdue University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslaa23main-p34-p doi:10.1145/3586033

User-Customizable Transpilation of Scripting Languages
Bo Wang, Aashish Kolluri, Ivica Nikolić, Teodora Baluta, and Prateek Saxena
(National University of Singapore, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslaa23main-p36-p doi:10.1145/3586034

Bidirectional Object-Oriented Programming: Towards Programmatic and Direct Manipulation of Objects
Xing Zhang, Guanchen Guo, Xiao He, and Zhenjiang Hu
(Peking University, China; University of Science and Technology Beijing, China)

Publisher's Version Published Artifact Artifacts Available Article: oopslaa23main-p37-p doi:10.1145/3586035

A Gradual Probabilistic Lambda Calculus
Wenjia Ye, Matías Toro, and Federico Olmedo
(University of Hong Kong, China; University of Chile, Chile)

Publisher's Version Article: oopslaa23main-p40-p doi:10.1145/3586036

Verus: Verifying Rust Programs using Linear Ghost Types
Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel
(VMware Research, Switzerland; Carnegie Mellon University, USA; ETH Zurich, Switzerland; UNSW Sydney, Australia; VMware Research, USA; Microsoft Research, USA)

Publisher's Version Published Artifact Archive submitted (61 kB) Artifacts Available Artifacts Reusable Article: oopslaa23main-p45-p doi:10.1145/3586037

Fat Pointers for Temporal Memory Safety of C
Jie Zhou, John Criswell, and Michael Hicks
(University of Rochester, USA; Amazon, USA; University of Maryland, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslaa23main-p64-p doi:10.1145/3586038

Modular Component-Based Quantum Circuit Synthesis
Chan Gu Kang and Hakjoo Oh
(Korea University, South Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslaa23main-p65-p doi:10.1145/3586039

A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations
Anthony C. J. Fox, Gareth Stockwell, Shale Xiong, Hanno Becker, Dominic P. Mulligan, Gustavo Petri, and Nathan Chong
(ARM, UK; Amazon Web Services, UK; Amazon Web Services, USA)

Publisher's Version Artifacts Reusable Article: oopslaa23main-p70-p doi:10.1145/3586040

Compositional Security Definitions for Higher-Order Where Declassification
Jan Menz, Andrew K. Hirsch, Peixuan Li, and Deepak Garg
(MPI-SWS, Germany; University at Buffalo, USA; Pennsylvania State University, USA)

Publisher's Version Article: oopslaa23main-p75-p doi:10.1145/3586041

Deep Learning Robustness Verification for Few-Pixel Attacks
Yuval Shapira, Eran Avneri, and Dana Drachsler-Cohen
(Technion, Israel)

Publisher's Version Article: oopslaa23main-p80-p doi:10.1145/3586042

Proof Automation for Linearizability in Separation Logic
Ike Mulder and Robbert Krebbers
(Radboud University Nijmegen, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslaa23main-p83-p doi:10.1145/3586043

Regular Expression Matching using Bit Vector Automata
Alexis Le Glaunec, Lingkun Kong, and Konstantinos Mamouras
(Rice University, USA)

Publisher's Version Artifacts Functional Article: oopslaa23main-p86-p doi:10.1145/3586044

Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
Noam Zilberstein, Derek Dreyer, and Alexandra Silva
(Cornell University, USA; MPI-SWS, Germany)

Publisher's Version Article: oopslaa23main-p89-p doi:10.1145/3586045

Aliasing Limits on Translating C to Safe Rust
Mehmet Emre, Peter Boyland, Aesha Parekh, Ryan Schroeder, Kyle Dewey, and Ben Hardekopf
(University of San Francisco, USA; University of California at Santa Barbara, USA; California State University, Northridge, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslaa23main-p91-p doi:10.1145/3586046

Automated Translation of Functional Big Data Queries to SQL
Guoqiang Zhang, Benjamin Mariano, Xipeng Shen, and Işıl Dillig
(North Carolina State University, USA; University of Texas at Austin, USA)

Publisher's Version Archive submitted (880 kB) Article: oopslaa23main-p98-p doi:10.1145/3586047

Live Pattern Matching with Typed Holes
Yongwei Yuan, Scott Guest, Eric Griffis, Hannah Potter, David Moon, and Cyrus Omar
(Purdue University, USA; University of Michigan, USA; University of Washington, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslaa23main-p103-p doi:10.1145/3586048

Pushing the Limit of 1-Minimality of Language-Agnostic Program Reduction
Zhenyang Xu, Yongqiang Tian, Mengxiao Zhang, Gaosen Zhao, Yu Jiang, and Chengnian Sun
(University of Waterloo, Canada; Tsinghua University, China)

Publisher's Version Published Artifact Artifacts Available Article: oopslaa23main-p117-p doi:10.1145/3586049

Exact Recursive Probabilistic Programming
David Chiang, Colin McDonald, and Chung-chieh Shan
(University of Notre Dame, USA; Indiana University, USA)

Publisher's Version Published Artifact Archive submitted (520 kB) Artifacts Available Artifacts Functional Article: oopslaa23main-p131-p doi:10.1145/3586050

Lower Bounds for Possibly Divergent Probabilistic Programs
Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Naijun Zhan
(Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Zhejiang University, China; Saarland University, Germany; University College London, UK; RWTH Aachen University, Germany)

Publisher's Version Article: oopslaa23main-p135-p doi:10.1145/3586051

Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs
Amir Kafshdar Goharshady, S. Hitarth, Fatemeh Mohammadi, and Harshit Jitendra Motwani
(Hong Kong University of Science and Technology, Hong Kong; KU Leuven, Belgium; Ghent University, Belgium)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslaa23main-p137-p doi:10.1145/3586052

Randomized Testing of Byzantine Fault Tolerant Algorithms
Levin N. Winter, Florena Buse, Daan de Graaf, Klaus von Gleissenthall, and Burcu Kulahcioglu Ozkan
(Delft University of Technology, Netherlands; Vrije Universiteit Amsterdam, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslaa23main-p151-p doi:10.1145/3586053

Verification-Preserving Inlining in Automatic Separation Logic Verifiers
Thibault Dardinier, Gaurav Parthasarathy, and Peter Müller
(ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslaa23main-p153-p doi:10.1145/3586054

Improving Oracle-Guided Inductive Synthesis by Efficient Question Selection
Ruyi Ji, Chaozhe Kong, Yingfei Xiong, and Zhenjiang Hu
(Peking University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslaa23main-p158-p doi:10.1145/3586055

Back to Direct Style: Typed and Tight
Marius Müller, Philipp Schuster, Jonathan Immanuel Brachthäuser, and Klaus Ostermann
(University of Tübingen, Germany)

Publisher's Version Article: oopslaa23main-p163-p doi:10.1145/3586056

Fluent APIs in Functional Languages
Ori Roth and Yossi Gil
(Technion, Israel)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslaa23main-p172-p doi:10.1145/3586057