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)

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)

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)

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)

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)

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

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

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)

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)

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)

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)

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)

Published Artifact Artifacts Available Artifacts Functional

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

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)

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)

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

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

Published Artifact Artifacts Available Artifacts Reusable

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

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)

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)

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)

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)

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)

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

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)

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)

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)

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)

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)

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)

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

Published Artifact Artifacts Available Artifacts Reusable