OOPSLA 2022
2022-12-05..2022-12-10
Auckland, New Zealand
OOPSLA ·
[OOPSLA 2018, OOPSLA 2020, OOPSLA 2021, OOPSLA 2022, OOPSLA 2023, OOPSLA 2024, OOPSLA 2025]
as the organisers put it
PACMPL Issue OOPSLA 2022 seeks contributions on all aspects of programming languages and software engineering. Authors of papers published in PACMPL Issue OOPSLA 2022 will be invited to present their work in the OOPSLA track of the SPLASH conference in December. Papers may target any stage of software development, including requirements, modeling, prototyping, design, implementation, generation, analysis, verification, testing, evaluation, maintenance, and reuse of software systems. Contributions may include the development of new tools (such as language front-ends, program analyses, and r ...
| title | author | length |
|---|---|---|
| Monadic and Comonadic Aspects of Dependency Analysis | Pritam Choudhury | 17m |
Presents GMCC, an alternative dependency calculus that is both monadic and comonadic, built from graded monads/comonads over a bicartesian closed category and… | ||
| Scalable Linear Invariant Generation with Farkas’ Lemma | Marshit Goshi | 18m |
Generates tight linear invariants for affine programs modeled as linear transition systems using Farkas' Lemma and keeps completeness while removing the… | ||
| Generic Go to Go: Dictionary-Passing, Monomorphisation, and Hybrid | Stephen Ellis, shofei nabuko, Lynn High | 23m |
Proposes a new dictionary-passing translation for Go generics that is type-, error- and value-preserving and proven correct by a novel bisimulation up to… | ||
| Neurosymbolic Repair for Low-Code Formula Languages | Harshit Joshi | 25m |
LaMirage generates repair engines from an annotated context free grammar plus small domain strategies, enumerates syntax-correct edits with a bounded… | ||
| SHARP: fast incremental context-sensitive pointer analysis for Java | Bozhen Liu, Jeff Huang | 18m |
SHARP is an incremental, context-sensitive pointer analysis for Java that claims to be the first to support k-CFA and k-obj under incremental code edits… | ||
| Modular Verification of Op-Based CRDTs in Separation Logic | Abel Nieto | 15m |
Framework verifies operation-based CRDT implementations in Coq using Aneris separation logic and a verified Reliable Causal Broadcast protocol plus an OpLib… | ||
| Oracle-Free Repair Synthesis for Floating-Point Programs | Daming Zhou | 14m |
Introduces microstructure — local neighborhoods where repeating floating-point error patterns let the tool infer accurate values without high-precision oracles… | ||
| Model Checking for a Multi-Execution Memory Model | Evgenii Moiseenko | 16m |
Introduces load buffering race freedom and certification locality as concrete constraints that rule out surprising out‑of‑thin‑air behaviors, defines a… | ||
| Coverage-guided tensor compiler fuzzing with joint IR-pass mutation | Java Liu | 14m |
Tzer mutates TVM’s low-level IR and the sequence of optimization passes together, using coverage feedback to prefer IR edits but switch to pass edits after a… | ||
| Type-Directed Synthesis of Visualizations from Natural Language Queries | Qiaochu Chen | 16m |
Graphy converts a natural-language query and a table into a ranked set of visualization programs by parsing intents and slots with a fine-tuned BERT into… | ||
| Consistency-Preserving Propagation for SMT Solving of Concurrent Program Verification | Sophia Drossopoulou | 13m |
Proposes consistency-preserving propagation that prevents self-loops in the ordering theory so consistency checking and conflict-clause generation become… | ||
| Reasoning about Distributed Reconfigurable Systems | Radu Iosif | 28m |
Claims a Hoare-style calculus for programs that create/delete nodes and connectors, using a resource logic in the spirit of separation logic and inductive… | ||
| A Fast In-Place Interpreter for WebAssembly | Ben L. Titzer | 29m |
Builds a handwritten-assembly in-place interpreter for WebAssembly called Wizards using Virgil and shows it runs as fast as many rewriting interpreters while… | ||
| Optimal Heap Limits for Reducing Browser Memory Use | Melissa kasame | 23m |
Proposes a concrete formula: set each heap limit to live size plus extra proportional to the square-root heap limit of live size, which provably minimizes… | ||
| The Road Not Taken: Exploring Alias Analysis Based Optimizations Missed by the Compiler | Khushboo Chitre, Piyus Kedia, Rahul Purandare | 25m |
Tool named Scout disambiguates two pointers at runtime with a single memory access by constraining allocation size and alignment via a segment-based allocator… | ||
| Complexity-guided container replacement synthesis | Chengpeng Wang, Peisen Yao, Wensheng Tang, Qingkai Shi, Charles Zhang | 30m |
Cres automatically synthesizes container-type replacements using static, allocation-based and flow-sensitive points-to analysis to collect container properties… | ||
| Katara: Synthesizing CRDTs with Verified Lifting | Shadaj Laddad, Conor Power, Mae Milano, Alvin Cheung, Joe Hellerstein | 22m |
Katara automatically synthesizes verified CRDTs from sequential data-type implementations and a pairwise operation ordering policy, encoding correctness into… | ||
| Specification-Guided Component-Based Synthesis from Effectful Libraries | Ashish Mishra, Suresh Jagannathan | 36m |
Cobalt implements Hoare-style pre/post specifications over OCaml libraries and combines spec-guided bi-directional search (backward weakest-pre to forward… | ||
| C to checked C by 3c | Aravind Machiry, John Kastner, Matt McCutchen, Aaron Eline, Kyle Headley, Michael Hicks | 30m |
3C is a static-analysis annotation tool that uses two novel algorithms, typ3c and boun3c, to infer Checked C pointer kinds and array bounds; it converts about… | ||
| Solo: A Lightweight Static Analysis for Differential Privacy | Chike Abuah, David Darais, Joseph P. Near | 28m |
Solo claims a practical, sound type system that enforces differential privacy inside Haskell without linear or relational refinement types. It encodes… | ||
| MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types | Lionel Parreaux, Chun Yin Chau | 32m |
MLstruct claims to combine principal polymorphic inference with first-class unions, intersections and equirecursive structural types by treating type… | ||
| Theoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning | Aleksander Boruch-Gruszecki, Radosław Waśko, Yichen Xu, Lionel Parreaux | 29m |
Introduces the cDOT calculus as a formal foundation that encodes subtyping information uncovered by pattern matching, builds on pDOT and DOT-style structural… | ||
| Coeffects for Sharing and Mutation | Riccardo Bianchini, Francesco Dagnino, Paola Giannini, Elena Zucca, Marco Servetto | 29m |
Coeffects model sharing in a Java-like calculus by representing effects as sets-of-links coeffects with a distinguished res link for result aliasing and… | ||
| Compilation of Dynamic Sparse Tensor Algebra | Stephen Chou, Saman Amarasinghe | 32m |
A compiler generates efficient tensor-algebra kernels from high-level node-schema language descriptions of recursive pointer-based layouts (block linked lists… | ||
| Incremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers | Aron Zwaan, Hendrik van Antwerpen, Eelco Visser | 25m |
Automatic derivation of incremental type-checkers from Statix meta-DSL specifications uses scope graphs to turn name-resolution queries into precise inter-unit… | ||
| UniRec: A Unimodular-Like Framework for Nested Recursions and Loops | Kirshanthan Sundararajah, Charitha Saumya, Milind Kulkarni | 31m |
Claim: UniRec generalizes unimodular loop transforms to mixed recursion+loop code and actually implements arbitrary unimodular linear schedules for recursive… | ||
| Checking Equivalence in a Non-strict Language | John C. Kolesar, Ruzica Piskac, William T. Hallahan | 21m |
Nebula implements a fully automated co-induction calculus and symbolic executor for equivalence checking in non-strict Haskell, proving 22 of 24 valid… | ||
| Necessity Specifications for Robustness | Julian Mackay, Susan Eisenbach, James Noble, Sophia Drossopoulou | 31m |
A formal language called necessity specifies robustness by stating explicit necessary preconditions: temporal-implication operators say exactly what must have… | ||
| Quantitative strongest post: a calculus for reasoning about the flow of quantitative inform | Linpeng Zhang, Benjamin Lucien Kaminski | 29m |
Presents a formal calculus that defines a quantitative strongest post and a strongest liberal post for nondeterministic programs with loops, where predicates… | ||
| A Study of Inline Assembly in Solidity Smart Contracts | Stefanos Chaliasos, Arthur Gervais, Ben Livshits | 27m |
A large-scale code audit of 6.8M contracts finds 23% of 6.8M contracts contain inline assembly, typically with up to three fragments per contract and 9–10… | ||
| Elipmoc: advanced decompilation of Ethereum smart contracts | Neville Grech, Sifis Lagouvardos, Ilias Tsatiris, Yannis Smaragdakis | 31m |
Elipmoc claims a practical, high-precision decompiler for Ethereum bytecode that resolves operands 99.5% of the time versus Gigahorse’s 62.8%, yields up to 67%… | ||
| SigVM: Enabling Event-Driven Execution for Truly Decentralized Smart Contracts | Zihan Zhao, Sidi Mohamed Beillahi, Ryan Song, Yuxi Cai, Andreas Veneris, Fan Long | 28m |
SigVM extends EVM with five primitives to create/delete signals, bind/detach handlers and emit events, making handlers execute automatically as signal… | ||
| Neural Architecture Search using Property Guided Synthesis | Charles Jin, Phitchaya Mangpo Phothilimthana, Sudip Roy | 30m |
αNAS performs evolutionary NAS by mutating abstract program properties (depth, shape, mixing) instead of raw graphs, concretizing candidates via a new… | ||
| Synthesizing Axiomatizations using Logic Learning | Paul Krogmeier, Zhengyao Lin, Adithya Murali, Madhusudan Parthasarathy | 29m |
A synthesis pipeline called the LAS framework combines a soundness checker, counterexample generator, independence checker and constraint-based logic learner… | ||
| Synthesizing fine-grained synchronization protocols for implicit monitors | Kostas Ferles, Benjamin Sepanski, Rahul Krishnan, James Bornholt, İsul Dillig | 31m |
A tool called Cortado statically proves safe interleavings by commutativity checks, builds a MaxSAT encoding that assigns locks per code snippet, and… | ||
| Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed | Aina Linn Georges, Alix Trieu, Lars Birkedal | 27m |
Introduces directed capabilities that add one extra bit and a single arithmetic bounds check to CHERI-style machines, enabling a calling convention that… | ||
| Plausible sealing for gradual parametricity | Elizabeth Labrada, Matías Toro, Éric Tanter, Dominique Devriese | 30m |
Proposes plausible sealing: postpone sealing decisions by inserting “maybe-seal” evidence so runtime, not static imprecision, decides whether a value is… | ||
| Purity of an ST monad: full abstraction by semantically typed back-translation | Koen Jacobs, Dominique Devriese, Amin Timany | 31m |
Proves that embedding a pure call-by-value language into an extension with an ST monad is fully abstract: contextual equivalences from the pure language remain… | ||
| Finding real bugs in big programs with incorrectness logic | Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, Peter W. O'Hearn | 29m |
Pulse-X applies ISL (a synthesis of Incorrectness Logic and separation logic) to build an automatic under-approximate analyzer for memory errors, inferring… | ||
| Fractional Resources in Unbounded Separation Logic | Thibault Dardinier, Peter Müller, Alexander J. Summers | 32m |
Defines a new semantics where assertions may temporarily use unbounded states that allow more-than-one permission during evaluation, then reimpose 0–1… | ||
| Proving Hypersafety Compositionally | Emanuele D'Osualdo, Azadeh Farzan, Derek Dreyer | 32m |
Claims a new proof system, the Logic for Hyper-triple Composition (LHC), that proves hypersafety properties compositionally by treating mixed-arity… | ||
| Bugs in Quantum computing platforms: an empirical study | Matteo Paltenghi, Michael Pradel | 27m |
Study inspects 223 real-world bugs from 18 open-source quantum platforms and finds 39.9% quantum-specific defects, concentrated in optimization and IR and… | ||
| Tower: Data Structures in Quantum Superposition | Charles Yuan, Michael Carbin | 25m |
Language Tower provides a reversible semantics that compiles every program to a unitary circuit and enforces reversible operations, a type system that bounds… | ||
| Verified Compilation of Quantum Oracles | Michael Hicks | 33m |
Verified compilation proves an imperative oracle language OQIMP compiles to OQASM and then to SQIR via Coq, preserving semantics and keeping simulation cost… | ||
| AnICA: Analyzing Inconsistencies in Microarchitectural Code Analyzers | Fabian Ritter, Sebastian Hack | 31m |
AnICA applies differential testing plus an abstract basic block generalization algorithm to compare llvm-mca, uiCA, Ithemal and similar predictors on 10,000… | ||
| Seq2Parse: Neurosymbolic Parse Error Repair | Georgios Sakkas, M. Endres, P. J. Guo, W. Weimer, R. Jhala | 38m |
Combines a neural sequence classifier that predicts a small subset of grammar-derived error rules with a symbolic error-correcting L-parser to synthesize… | ||
| BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs | Fengmin (Paul) Zhu, Michael Sammler, Derek Dreyer, Deepak Garg, Rodolphe Lepigre | 29m |
A foundational, automated verifier encodes common bitfield patterns as structured bit vectors and implements partial, semantics-preserving operations (masking… | ||
| Compositional Virtual Timelines: Verifying Dynamic-Priority Partitions with Algorithmic Tem | Mengqi Liu, Zhong Shao, Hao Chen, Man-Ki Yoon, Jung-Eun Kim | 27m |
Claims a formally verified real-time OS kernel that enforces budget-enforcing EDF partitions and proves temporal isolation between partitions under the… | ||
| Linear types for large-scale systems verification | JIALIN LI, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, Chris Hawblitzel | 32m |
Integrates linear Dafny with Dafny's SMT backend to push memory reasoning into the type system while keeping SMT for heap invariants; implements… | ||
| Effects,capabilities,and boxes: from scope-based reasoning to type-based reasoning and back | Aleksander Boruch-Gruszecki | 30m |
Claims a middle ground: System C reconciling capability-based and traditional effect systems by tracking which lexical capabilities a binding transitively… | ||
| First-class Names for Effect Handlers | Ningning Xie, Youyou Cong, Kazuki Ikemori, Daan Leijen | 28m |
Claim: treating first-class handler names as values plus scoped effects with rank-2 polymorphism prevents name-escaping without new language primitives. Paper… | ||
| High-Level Effect Handlers in C++ | Sam Lindley | 32m |
cpp-effects is a C++ library that implements deep, affine effect handlers on top of boost.context fibers, with handlers expressed as classes using multiple… | ||
| Semi-symbolic Inference for Efficient Streaming Probabilistic Programming | Eric Atkinson, Charles Yuan, Guillaume Baudart, Louis Mandel, Michael Carbin | 26m |
Semi-symbolic inference implements an automatic Rao-Blackwellized particle filter in ProbZelus by manipulating symbolic expression trees, using a central swap… | ||
| Symbolic Execution for Randomized Programs | Zachary Susag, Justin Hsu, Sumit Lahiri, Subhajit Roy | 34m |
Adds probabilistic symbolic variables to symbolic execution and computes symbolic probability expressions for paths, then checks universal quantitative… | ||
| This Is the Moment for Probabilistic Loops | Miroslav Stanković, Ezio Bartocci, Laura Kovács, Marcel Moosbrugger | 30m |
Static analysis derives exact higher moments for many probabilistic loops, producing closed‑form expressions and tail bounds automatically without templates or… | ||
| A Concurrent Program Logic with a Future and History | Roland Meyer, Thomas Wies, Sebastian Wolff | 24m |
A new separation logic that preserves local reasoning while enabling automation introduces ghost update chunks to decompose unbounded physical removals into… | ||
| CAAT: Consistency as a Theory | Thomas Haas, Roland Meyer, Hernán Ponce de León | 28m |
Claims a family of logical theories that capture memory-model consistency (TSO, POWER, ARMv8, RISC‑V, RC11, IMM, Linux kernel) and builds a generic, efficient… | ||
| Implementing and Verifying Release-Acquire Transactional Memory in C11 | Sadegh Dalvandi, Brijesh Dongol | 30m |
Defines a relaxed transactional-memory spec called TMS2-ra integrated with RC11 (view-based RC11) and a program logic TARO, implements the spec as a C11… | ||
| Data-Driven Lemma Synthesis for Interactive Proofs | Aishwarya Sivaraman, Alex Sanchez-Stern, Bretton Chen, Sorin Lerner, Todd Millstein | 26m |
A tool called lfind as a Coq tactic reduces lemma synthesis to a data-driven program synthesis problem: it generalizes a stuck goal, generates input/output… | ||
| Intrinsically-Typed Definitional Interpreters à la Carte | Cas van der Rest, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser, Peter D. Mosses | 33m |
Presents a method for building modular, mechanically verified type-safe language components using intrinsically-typed definitional interpreters and a new… | ||
| Proof transfer for fast certification of multiple approximate neural networks | Shubham Ugare, Gagandeep Singh, Sasa Misailovic | 25m |
FANC generates templates—connected symbolic shapes at an intermediate layer—and a cheap template transformer that adapts those templates to approximate… | ||
| Can Guided Decomposition Help End-Users Write Larger Block-Based Programs? A Mobile Robot E | Nico Ritschel, Felipe Fronchetti, Reid Holmes, Ronald Garcia, David C. Shepherd | 32m |
A block-based mobile-robot editor with two-canvas guided decomposition and a simulator is built and tested on 92 MTurk participants; the claim is that… | ||
| Compositional Embeddings of Domain-Specific Languages | Yaozhu Sun, Utkarsh Dhandhania, Bruno C. d. S. Oliveira | 27m |
Claims a compositional embedding implemented in the CP language that combines shallow and deep benefits by typing constructors with an abstract sort and… | ||
| Language-parametric static semantic code completion | Daniel A. A. Pelsmaeker, Hendrik van Antwerpen, Casper Bach Poulsen, Eelco Visser | 29m |
Implements a language‑parametric code completion that is sound and complete by construction: it reinterprets Statix static semantics and SDF3 syntax to expand… | ||
| Overwatch: Learning Patterns in Code Edit Sequences | Yuhao Zhang, Yasharth Bajpai, Priyanshu Gupta, Ameya Ketkar, Miltiadis Allamanis, Titus Barik, Sumit Gulwani, Arjun Radhakrishna, Mohammad Raza, Gustavo Soares, Ashish Tiwari | 30m |
Overwatch learns recurring edit sequences from IDE session traces by building fine-grained edit graphs, summarizing them into an edit quotient graph… | ||
| Satisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing | Sujit Kumar Muduli, Subhajit Roy | 22m |
A solver, Sādhak, couples an SMT engine (built on CVC4) with a fuzzer (AFL++) to handle closed-box functions by compiling expressions to small programs and… | ||
| Synthesizing Code Quality Rules from Examples | Pranav Garg, Srinivasan H. Sengamedu | 32m |
Automatic synthesis of code-quality rules from code-change examples produces executable graph queries now deployed in Amazon CodeGuru Reviewer. The system uses… | ||
| C4: verified transactional objects | Mohsen Lesani, Li-yao Xia, Anders Kaseorg, C.J. Bell, Adam Chlipala, Benjamin Pierce, Steve Zdancewic | 27m |
C4 claims a mechanized, compositional way to prove both linearizability and strict serializability and to stitch those proofs together for mixed… | ||
| Concurrent Size | Gal Sela, Erez Petrank | 32m |
Presents a methodology that adds a linearizable size operation to sets and dictionaries by publishing small metadata per thread and using a snapshot of… | ||
| Veracity: Declarative Multicore Programming with Commutativity | Adam Chen, Parisa Fathololumi, Eric Koskinen, Jared Pincus | 27m |
A new language, Veracity (implemented in Multicore OCaml), lets programmers mark commute blocks with logical predicates and the compiler either forks them or… | ||
| On incorrectness logic for Quantum programs | Peng Yan, Hanru Jiang, Nengkun Yu | 30m |
Proposes an incorrectness logic for quantum programs that treats predicates as projections and defines an under-approximation by projections relation to… | ||
| Weighted programming: a programming paradigm for specifying mathematical models | Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Tobias Winkler | 28m |
Defines an imperative language with nondeterministic branching and weighted traces parameterized by a semiring, and gives a denotational semantics via a… | ||
| Wildcards Need Witness Protection | Kevin Bierhoff | 28m |
Claim: Java's wildcard unsoundness is avoidable by requiring every wildcard to have a witness type when introduced (including from null), formalized in a core… | ||
| Automated transpilation of imperative to functional code using neural-guided program synthe | Benjamin Mariano, Yanju Chen, Yu Feng, Greg Durrett, Isil Dillig | 28m |
A tool called NGST2 implements a neural-guided synthesizer that converts imperative Java and Python snippets into Stream and functools pipelines by assuming… | ||
| Synthesis-Powered Optimization of Smart Contracts via Data Type Refactoring | Yanju Chen, Yuepeng Wang, Maruth Goyal, James Dong, Yu Feng, Isil Dillig | 29m |
Tool called Solidare uses a small DSL plus optimal program synthesis (sketch generation, sketch completion, equivalence checking) and a static gas-cost proxy… | ||
| Synthesizing Abstract Transformers | Pankaj Kumar Kalita, Sujit Kumar Muduli, Loris D'Antoni, Thomas Reps, Subhajit Roy | 28m |
Method synthesizes an abstract transformer from (i) a concrete semantics for op, (ii) an abstract domain A, and (iii) a DSL L, producing an AMURTH output that… | ||
| Indexing the Extended Dyck-CFL Reachability for Context-Sensitive Program Analysis | Qingkai Shi, Yongchao Wang, Peisen Yao, Charles Zhang, Chengpeng Wang | 31m |
This paper presents a cheap reduction that transforms extended Dyck-CFL reachability to conventional graph reachability, builds a two-copy indexed graph with… | ||
| The Essence of Online Data Processing | Philip Dexter, Yu David Liu, Kenneth Chiu | 27m |
Claims a first rigorous foundation called DON Calculus for online data processing that models backend and frontend behavior and centers on IOP and TLO. The key… | ||
| Taming Transitive Redundancy for Context-Free Language Reachability | Yuxiang Lei, Yulei Sui, Shuo Ding, Qirun Zhang | 15m |
CFL-reachability uses on-the-fly edge derivation; this work introduces POCR running on a hybrid spanning-tree + adjacency-list representation to enforce a… | ||
| A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in | Dan Frumin, Emanuele D'Osualdo, Bas van den Heuvel, Jorge A. Pérez | 28m |
A session-typed π-calculus extracted from the Logic of Bunched Implications, called πBI, implements a new runtime spawn primitive that duplicates providers… | ||
| nothing matches | ||