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

Proceedings of the ACM on Programming Languages, Volume 6, Number OOPSLA1, December 8–10, 2022, Auckland, New Zealand

OOPSLA – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message

Papers

Weighted Programming: A Programming Paradigm for Specifying Mathematical Models
Kevin Batz ORCID logo, Adrian Gallus ORCID logo, Benjamin Lucien KaminskiORCID logo, Joost-Pieter Katoen ORCID logo, and Tobias Winkler ORCID logo
(RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK)
Publisher's Version
Synthesizing Fine-Grained Synchronization Protocols for Implicit Monitors
Kostas FerlesORCID logo, Benjamin SepanskiORCID logo, Rahul Krishnan ORCID logo, James BornholtORCID logo, and Işil Dillig ORCID logo
(University of Texas at Austin, USA)
Publisher's Version Info
Complexity-Guided Container Replacement Synthesis
Chengpeng WangORCID logo, Peisen YaoORCID logo, Wensheng Tang ORCID logo, Qingkai ShiORCID logo, and Charles ZhangORCID logo
(Hong Kong University of Science and Technology, China; Ant Group, China)
Publisher's Version
Linear Types for Large-Scale Systems Verification
Jialin Li ORCID logo, Andrea Lattuada ORCID logo, Yi Zhou ORCID logo, Jonathan Cameron ORCID logo, Jon Howell ORCID logo, Bryan ParnoORCID logo, and Chris Hawblitzel ORCID logo
(University of Washington, USA; ETH Zurich, Switzerland; Carnegie Mellon University, USA; VMware Research, USA; Microsoft Research, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Plausible Sealing for Gradual Parametricity
Elizabeth Labrada ORCID logo, Matías Toro ORCID logo, Éric TanterORCID logo, and Dominique DevrieseORCID logo
(University of Chile, Chile; KU Leuven, Belgium)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Automated Transpilation of Imperative to Functional Code using Neural-Guided Program Synthesis
Benjamin Mariano ORCID logo, Yanju Chen ORCID logo, Yu FengORCID logo, Greg Durrett ORCID logo, and Işil Dillig ORCID logo
(University of Texas at Austin, USA; University of California at Santa Barbara, USA)
Publisher's Version
On Incorrectness Logic for Quantum Programs
Peng Yan ORCID logo, Hanru Jiang ORCID logo, and Nengkun Yu ORCID logo
(University of Technology Sydney, Australia; BIMSA, China)
Publisher's Version
Coverage-Guided Tensor Compiler Fuzzing with Joint IR-Pass Mutation
Jiawei LiuORCID logo, Yuxiang Wei ORCID logo, Sen Yang ORCID logo, Yinlin Deng ORCID logo, and Lingming Zhang ORCID logo
(University of Illinois at Urbana-Champaign, USA; Tongji University, China; Fudan University, China)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities
Aïna Linn Georges ORCID logo, Alix TrieuORCID logo, and Lars BirkedalORCID logo
(Aarhus University, Denmark; ANSSI, France)
Publisher's Version Published Artifact Archive submitted (440 kB) Artifacts Available Artifacts Reusable
Proof Transfer for Fast Certification of Multiple Approximate Neural Networks
Shubham UgareORCID logo, Gagandeep SinghORCID logo, and Sasa MisailovicORCID logo
(University of Illinois at Urbana-Champaign, USA; VMware Research, USA)
Publisher's Version
Effects, Capabilities, and Boxes: From Scope-Based Reasoning to Type-Based Reasoning and Back
Jonathan Immanuel BrachthäuserORCID logo, Philipp Schuster ORCID logo, Edward Lee ORCID logo, and Aleksander Boruch-Gruszecki ORCID logo
(University of Tübingen, Germany; University of Waterloo, Canada; EPFL, Switzerland)
Publisher's Version Published Artifact Archive submitted (1.1 MB) Info Artifacts Available Artifacts Reusable
Elipmoc: Advanced Decompilation of Ethereum Smart Contracts
Neville Grech ORCID logo, Sifis Lagouvardos ORCID logo, Ilias Tsatiris ORCID logo, and Yannis Smaragdakis ORCID logo
(University of Malta, Malta; University of Athens, Greece)
Publisher's Version Artifacts Reusable
C to Checked C by 3C
Aravind MachiryORCID logo, John Kastner ORCID logo, Matt McCutchen ORCID logo, Aaron Eline ORCID logo, Kyle Headley ORCID logo, and Michael Hicks ORCID logo
(Purdue University, USA; Amazon, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Applying Cognitive Principles to Model-Finding Output: The Positive Value of Negative Information
Tristan Dyer ORCID logo, Tim Nelson ORCID logo, Kathi Fisler ORCID logo, and Shriram Krishnamurthi ORCID logo
(Brown University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
C4: Verified Transactional Objects
Mohsen Lesani ORCID logo, Li-yao Xia ORCID logo, Anders Kaseorg, Christian J. Bell, Adam ChlipalaORCID logo, Benjamin C. PierceORCID logo, and Steve ZdancewicORCID logo
(University of California at Riverside, USA; University of Pennsylvania, USA; Massachusetts Institute of Technology, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Finding Real Bugs in Big Programs with Incorrectness Logic
Quang Loc Le ORCID logo, Azalea RaadORCID logo, Jules Villard ORCID logo, Josh Berdine ORCID logo, Derek DreyerORCID logo, and Peter W. O'Hearn ORCID logo
(University College London, UK; Meta, UK; Imperial College London, UK; MPI-SWS, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Purity of an ST Monad: Full Abstraction by Semantically Typed Back-Translation
Koen Jacobs ORCID logo, Dominique DevrieseORCID logo, and Amin TimanyORCID logo
(KU Leuven, Belgium; Aarhus University, Denmark)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable
Translating Canonical SQL to Imperative Code in Coq
Véronique Benzaken ORCID logo, Évelyne Contejean ORCID logo, Mohammed Houssem Hachmaoui ORCID logo, Chantal KellerORCID logo, Louis Mandel ORCID logo, Avraham Shinnar ORCID logo, and Jérôme Siméon ORCID logo
(LMF, France; Université Paris-Saclay, France; CNRS, France; IBM Research, USA; Docusign, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
End-to-End Translation Validation for the Halide Language
Basile ClémentORCID logo and Albert Cohen ORCID logo
(Inria, France; ENS Paris, France; Google, France)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Language-Parametric Static Semantic Code Completion
Daniel A. A. Pelsmaeker ORCID logo, Hendrik van Antwerpen ORCID logo, Casper Bach Poulsen ORCID logo, and Eelco Visser ORCID logo
(Delft University of Technology, Netherlands)
Publisher's Version Published Artifact Archive submitted (120 kB) Artifacts Available Artifacts Functional
Bugs in Quantum Computing Platforms: An Empirical Study
Matteo PaltenghiORCID logo and Michael Pradel ORCID logo
(University of Stuttgart, Germany)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable
Quantitative Strongest Post: A Calculus for Reasoning about the Flow of Quantitative Information
Linpeng ZhangORCID logo and Benjamin Lucien KaminskiORCID logo
(University College London, UK; Saarland University, Germany)
Publisher's Version
SHARP: Fast Incremental Context-Sensitive Pointer Analysis for Java
Bozhen Liu ORCID logo and Jeff Huang ORCID logo
(Texas A&M University, USA)
Publisher's Version
Functional Collection Programming with Semi-ring Dictionaries
Amir Shaikhha ORCID logo, Mathieu Huot ORCID logo, Jaclyn Smith ORCID logo, and Dan Olteanu ORCID logo
(University of Edinburgh, UK; University of Oxford, UK; University of Zurich, Switzerland)
Publisher's Version

proc time: 4.9