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

Title Page

Editorial Message

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

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

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

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

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

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

Publisher's Version

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

Publisher's Version

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

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

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

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

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

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

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

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

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

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

Publisher's Version

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

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

Publisher's Version Artifacts Functional

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

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

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)

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

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

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) Info Artifacts Available Artifacts Functional

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

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

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

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

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

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

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable