OOPSLA1 2023
Proceedings of the ACM on Programming Languages, Volume 7, Number OOPSLA1
Powered by
Conference Publishing Consulting

Proceedings of the ACM on Programming Languages, Volume 7, Number OOPSLA1, October 22–27, 2023, Cascais, Portugal

OOPSLAA – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message

Papers

Accelerating Fuzzing through Prefix-Guided Execution
Shaohua Li ORCID logo and Zhendong Su ORCID logo
(ETH Zurich, Switzerland)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Solving Conditional Linear Recurrences for Program Verification: The Periodic Case
Chenglin Wang ORCID logo and Fangzhen Lin ORCID logo
(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 ORCID logo, Xiaohong ChenORCID logo, Minh-Thai Trinh ORCID logo, John Wang ORCID logo, and Grigore Roşu ORCID logo
(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 BarkeORCID logo, Michael B. JamesORCID logo, and Nadia PolikarpovaORCID logo
(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 GheriORCID logo and Nobuko Yoshida ORCID logo
(University of Oxford, UK)
Publisher's Version
Languages with Decidable Learning: A Meta-theorem
Paul Krogmeier ORCID logo and P. MadhusudanORCID logo
(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 ORCID logo, Nouraldin Jaber ORCID logo, and Roopsha Samanta ORCID logo
(Purdue University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
User-Customizable Transpilation of Scripting Languages
Bo Wang ORCID logo, Aashish Kolluri ORCID logo, Ivica Nikolić ORCID logo, Teodora Baluta ORCID logo, and Prateek SaxenaORCID logo
(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 ORCID logo, Guanchen Guo ORCID logo, Xiao He ORCID logo, and Zhenjiang Hu ORCID logo
(Peking University, China; University of Science and Technology Beijing, China)
Publisher's Version Published Artifact Artifacts Available
A Gradual Probabilistic Lambda Calculus
Wenjia Ye ORCID logo, Matías Toro ORCID logo, and Federico Olmedo ORCID logo
(University of Hong Kong, China; University of Chile, Chile)
Publisher's Version
Verus: Verifying Rust Programs using Linear Ghost Types
Andrea Lattuada ORCID logo, Travis Hance ORCID logo, Chanhee Cho ORCID logo, Matthias Brun ORCID logo, Isitha Subasinghe ORCID logo, Yi Zhou ORCID logo, Jon Howell ORCID logo, Bryan ParnoORCID logo, and Chris Hawblitzel ORCID logo
(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 ORCID logo, John Criswell ORCID logo, and Michael HicksORCID logo
(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 ORCID logo and Hakjoo Oh ORCID logo
(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 ORCID logo, Gareth Stockwell ORCID logo, Shale Xiong ORCID logo, Hanno Becker ORCID logo, Dominic P. Mulligan ORCID logo, Gustavo Petri ORCID logo, and Nathan Chong ORCID logo
(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 ORCID logo, Andrew K. Hirsch ORCID logo, Peixuan Li ORCID logo, and Deepak GargORCID logo
(MPI-SWS, Germany; University at Buffalo, USA; Pennsylvania State University, USA)
Publisher's Version
Deep Learning Robustness Verification for Few-Pixel Attacks
Yuval Shapira ORCID logo, Eran Avneri ORCID logo, and Dana Drachsler-Cohen ORCID logo
(Technion, Israel)
Publisher's Version
Proof Automation for Linearizability in Separation Logic
Ike MulderORCID logo and Robbert KrebbersORCID logo
(Radboud University Nijmegen, Netherlands)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Regular Expression Matching using Bit Vector Automata
Alexis Le Glaunec ORCID logo, Lingkun KongORCID logo, and Konstantinos Mamouras ORCID logo
(Rice University, USA)
Publisher's Version Artifacts Functional
Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
Noam Zilberstein ORCID logo, Derek DreyerORCID logo, and Alexandra Silva ORCID logo
(Cornell University, USA; MPI-SWS, Germany)
Publisher's Version
Aliasing Limits on Translating C to Safe Rust
Mehmet Emre ORCID logo, Peter Boyland ORCID logo, Aesha Parekh ORCID logo, Ryan Schroeder ORCID logo, Kyle Dewey ORCID logo, and Ben Hardekopf ORCID logo
(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 ORCID logo, Benjamin Mariano ORCID logo, Xipeng ShenORCID logo, and Işıl Dillig ORCID logo
(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 ORCID logo, Scott Guest ORCID logo, Eric Griffis ORCID logo, Hannah Potter ORCID logo, David Moon ORCID logo, and Cyrus OmarORCID logo
(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 ORCID logo, Yongqiang Tian ORCID logo, Mengxiao Zhang ORCID logo, Gaosen Zhao ORCID logo, Yu Jiang ORCID logo, and Chengnian Sun ORCID logo
(University of Waterloo, Canada; Tsinghua University, China)
Publisher's Version
Exact Recursive Probabilistic Programming
David Chiang ORCID logo, Colin McDonald ORCID logo, and Chung-chieh Shan ORCID logo
(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 ORCID logo, Mingshuai Chen ORCID logo, Han Su ORCID logo, Benjamin Lucien Kaminski ORCID logo, Joost-Pieter Katoen ORCID logo, and Naijun Zhan ORCID logo
(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 ORCID logo, S. Hitarth ORCID logo, Fatemeh Mohammadi ORCID logo, and Harshit Jitendra Motwani ORCID logo
(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 ORCID logo, Florena Buse ORCID logo, Daan de Graaf ORCID logo, Klaus von Gleissenthall ORCID logo, and Burcu Kulahcioglu Ozkan ORCID logo
(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 DardinierORCID logo, Gaurav Parthasarathy ORCID logo, and Peter Müller ORCID logo
(ETH Zurich, Switzerland)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Improving Oracle-Guided Inductive Synthesis by Efficient Question Selection
Ruyi Ji ORCID logo, Chaozhe Kong ORCID logo, Yingfei Xiong ORCID logo, and Zhenjiang Hu ORCID logo
(Peking University, China)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Back to Direct Style: Typed and Tight
Marius Müller ORCID logo, Philipp Schuster ORCID logo, Jonathan Immanuel Brachthäuser ORCID logo, and Klaus Ostermann ORCID logo
(University of Tübingen, Germany)
Publisher's Version
Fluent APIs in Functional Languages
Ori Roth ORCID logo and Yossi Gil ORCID logo
(Technion, Israel)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

proc time: 7.8