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)

Article Search 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)

Article Search 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)

Article Search 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)

Article Search Artifacts Available Artifacts Reusable

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

Article Search

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

Article Search

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

Article Search 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)

Article Search 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)

Preprint Artifacts Available

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

Article Search

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)

Article Search 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)

Article Search Artifacts Available Artifacts Functional

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

Article Search 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)

Article Search 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)

Preprint

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

Article Search

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

Article Search Artifacts Available Artifacts Reusable

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

Article Search 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)

Article Search

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)

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

Article Search 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)

Article Search 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)

Article Search Artifacts Available

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

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

Preprint

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)

Article Search 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)

Article Search Artifacts Available Artifacts Reusable

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

Article Search 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)

Article Search 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)

Preprint

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

Preprint Artifacts Available Artifacts Reusable