OOPSLA1 2022
Proceedings of the ACM on Programming Languages, Volume 6, Number OOPSLA1

Title Page

Article: oopsla22foreword-fm000-p doi:

Editorial Message

Article: oopsla22foreword-fm001-p doi:

Weighted Programming: A Programming Paradigm for Specifying Mathematical Models
Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Tobias Winkler
(RWTH Aachen University, Germany; Saarland University, Germany; University College London, UK)

Publisher's Version Article: oopsla22main-p9-p doi:10.1145/3527310

Synthesizing Fine-Grained Synchronization Protocols for Implicit Monitors
Kostas Ferles, Benjamin Sepanski, Rahul Krishnan, James Bornholt, and Işil Dillig
(University of Texas at Austin, USA)

Publisher's Version Article: oopsla22main-p21-p doi:10.1145/3527311

Complexity-Guided Container Replacement Synthesis
Chengpeng Wang, Peisen Yao, Wensheng Tang, Qingkai Shi, and Charles Zhang
(Hong Kong University of Science and Technology, China; Ant Group, China)

Publisher's Version Article: oopsla22main-p28-p doi:10.1145/3527312

Linear Types for Large-Scale Systems Verification
Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, and Chris Hawblitzel
(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 Article: oopsla22main-p29-p doi:10.1145/3527313

Plausible Sealing for Gradual Parametricity
Elizabeth Labrada, Matías Toro, Éric Tanter, and Dominique Devriese
(University of Chile, Chile; KU Leuven, Belgium)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopsla22main-p32-p doi:10.1145/3527314

Automated Transpilation of Imperative to Functional Code using Neural-Guided Program Synthesis
Benjamin Mariano, Yanju Chen, Yu Feng, Greg Durrett, and Işil Dillig
(University of Texas at Austin, USA; University of California at Santa Barbara, USA)

Publisher's Version Article: oopsla22main-p37-p doi:10.1145/3527315

On Incorrectness Logic for Quantum Programs
Peng Yan, Hanru Jiang, and Nengkun Yu
(University of Technology Sydney, Australia; BIMSA, China)

Publisher's Version Article: oopsla22main-p38-p doi:10.1145/3527316

Coverage-Guided Tensor Compiler Fuzzing with Joint IR-Pass Mutation
Jiawei Liu, Yuxiang Wei, Sen Yang, Yinlin Deng, and Lingming Zhang
(University of Illinois at Urbana-Champaign, USA; Tongji University, China; Fudan University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopsla22main-p41-p doi:10.1145/3527317

Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities
Aïna Linn Georges, Alix Trieu, and Lars Birkedal
(Aarhus University, Denmark; ANSSI, France)

Publisher's Version Published Artifact Archive submitted (440 kB) Artifacts Available Artifacts Reusable Article: oopsla22main-p45-p doi:10.1145/3527318

Proof Transfer for Fast Certification of Multiple Approximate Neural Networks
Shubham Ugare, Gagandeep Singh, and Sasa Misailovic
(University of Illinois at Urbana-Champaign, USA; VMware Research, USA)

Publisher's Version Article: oopsla22main-p46-p doi:10.1145/3527319

Effects, Capabilities, and Boxes: From Scope-Based Reasoning to Type-Based Reasoning and Back
Jonathan Immanuel Brachthäuser, Philipp Schuster, Edward Lee, and Aleksander Boruch-Gruszecki
(University of Tübingen, Germany; University of Waterloo, Canada; EPFL, Switzerland)

Publisher's Version Published Artifact Archive submitted (1.1 MB) Artifacts Available Artifacts Reusable Article: oopsla22main-p53-p doi:10.1145/3527320

Elipmoc: Advanced Decompilation of Ethereum Smart Contracts
Neville Grech, Sifis Lagouvardos, Ilias Tsatiris, and Yannis Smaragdakis
(University of Malta, Malta; University of Athens, Greece)

Publisher's Version Artifacts Reusable Article: oopsla22main-p55-p doi:10.1145/3527321

C to Checked C by 3C
Aravind Machiry, John Kastner, Matt McCutchen, Aaron Eline, Kyle Headley, and Michael Hicks
(Purdue University, USA; Amazon, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopsla22main-p59-p doi:10.1145/3527322

Applying Cognitive Principles to Model-Finding Output: The Positive Value of Negative Information
Tristan Dyer, Tim Nelson, Kathi Fisler, and Shriram Krishnamurthi
(Brown University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopsla22main-p64-p doi:10.1145/3527323

C4: Verified Transactional Objects
Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic
(University of California at Riverside, USA; University of Pennsylvania, USA; Massachusetts Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopsla22main-p66-p doi:10.1145/3527324

Finding Real Bugs in Big Programs with Incorrectness Logic
Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn
(University College London, UK; Meta, UK; Imperial College London, UK; MPI-SWS, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopsla22main-p77-p doi:10.1145/3527325

Purity of an ST Monad: Full Abstraction by Semantically Typed Back-Translation
Koen Jacobs, Dominique Devriese, and Amin Timany
(KU Leuven, Belgium; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopsla22main-p78-p doi:10.1145/3527326

Translating Canonical SQL to Imperative Code in Coq
Véronique Benzaken, Évelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, and Jérôme Siméon
(LMF, France; Université Paris-Saclay, France; CNRS, France; IBM Research, USA; Docusign, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopsla22main-p90-p doi:10.1145/3527327

End-to-End Translation Validation for the Halide Language
Basile Clément and Albert Cohen
(Inria, France; ENS Paris, France; Google, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopsla22main-p96-p doi:10.1145/3527328

Language-Parametric Static Semantic Code Completion
Daniel A. A. Pelsmaeker, Hendrik van Antwerpen, Casper Bach Poulsen, and Eelco Visser
(Delft University of Technology, Netherlands)

Publisher's Version Published Artifact Archive submitted (120 kB) Artifacts Available Artifacts Functional Article: oopsla22main-p98-p doi:10.1145/3527329

Bugs in Quantum Computing Platforms: An Empirical Study
Matteo Paltenghi and Michael Pradel
(University of Stuttgart, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopsla22main-p104-p doi:10.1145/3527330

Quantitative Strongest Post: A Calculus for Reasoning about the Flow of Quantitative Information
Linpeng Zhang and Benjamin Lucien Kaminski
(University College London, UK; Saarland University, Germany)

Publisher's Version Article: oopsla22main-p132-p doi:10.1145/3527331

SHARP: Fast Incremental Context-Sensitive Pointer Analysis for Java
Bozhen Liu and Jeff Huang
(Texas A&M University, USA)

Publisher's Version Article: oopsla22main-p149-p doi:10.1145/3527332

Functional Collection Programming with Semi-ring Dictionaries
Amir Shaikhha, Mathieu Huot, Jaclyn Smith, and Dan Olteanu
(University of Edinburgh, UK; University of Oxford, UK; University of Zurich, Switzerland)

Publisher's Version Article: oopsla22main-p159-p doi:10.1145/3527333