PLDI 2022
2022-06-13..2022-06-17
San Diego, United States
[PLDI 2020, PLDI 2022, PLDI 2023, PLDI 2024, PLDI 2024 Workshop Honoring Andreas Podelski, PLDI 2025, PLDI 2026, PLDI 2026 Student Research Competition]
as the organisers put it
Welcome to the home page of the 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2022)! PLDI is the premier forum in the field of programming languages and programming systems research, covering the areas of design, implementation, theory, applications, and performance. PLDI 2022 will be held in-person at the Catamaran Resort in San Diego, California, USA. PLDI 2022 Guides Attendees Speakers Session Chairs Registration Early registration ends on May 16. Click here to register. Virtual Participation If you cannot join us in-person, you can register to p ...
| title | author | length |
|---|---|---|
| A Flexible Type System for Fearless Concurrency | Mei Milano, Josh Takati, Andrew C. Myers | 19m |
A type system eliminates destructive data races by treating whole regions as affine resources and tracking exact broken paths with a focus mechanism, requiring… | ||
| A Study of Real-world Data Races in Golang | I'm melanch | 19m |
Deploys Go's dynamic race detector (ThreadSanitizer via Go's -race) across a 57M‑LOC monorepo, compiling and running unit tests daily, and reports 3.5k races… | ||
| A Typed Continuation-Passing Translation for Lexical Effect Handlers | Philipp Schuster, Jonathan Immanuel Brachthäuser, Marius Müller, Klaus Ostermann | 17m |
Claims a sound translation of lexical effect handlers to pure System F via a continuation-passing translation that needs no runtime support. Handlers, regions… | ||
| Abstract Interpretation Repair | Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Francesco Ranzato | 20m |
This work gives an algorithmic way to repair abstract interpreters by add one point u into the abstract domain along a program trace, producing the minimal… | ||
| Adore: Atomic Distributed Objects with Certified Reconfiguration | Wolf Honore | 18m |
Presents Adore, an object-level abstraction that yields the first safety proof with hot reconfiguration by formalizing a cache-tree model and three concrete… | ||
| Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra | ishan pong, mission a | 18m |
Encodes quantum while programs into algebraic expressions and proves soundness: derivability in non-idempotent Kleene algebra implies denotational equivalence… | ||
| ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification | Sankha Narayan Guria, Niki Vazou, Marco Guarnieri, James Parker | 18m |
ANOSY verifies attacker-knowledge approximations and synthesizes posterior-update functions using refinement types, then checks them with Liquid Haskell and an… | ||
| Type-Directed Program Synthesis for RESTful APIs | Zheng Guo, David Cao, Davin Tjong, Jean Yang, Cole Schlesinger, Nadia Polikarpova | 20m |
Built a tool called epiphany that infers fine-grained semantic types from OpenAPI docs plus thousands of observed API call traces, uses a type-directed… | ||
| Autoscheduling for Sparse Tensor Algebra with an Asymptotic Cost Model | Kiran Prasad, Carson McCrosky, Sanjay Kale, Sanjib Sinha, Sanket Agrawal | 18m |
The paper builds an autoscheduler that models sparse tensor runtimes as sets of iteration tasks and picks schedules by comparing those sets, using asymptotic… | ||
| Bind the Gap: Compiling Real Software to Hardware FFT Accelerators | Joseph E. Gonzalez, Luis Ceze, Kunal Agrawal, Kevin Lim, Markus M. Alameldeen | 19m |
Paper claims a compiler pipeline that automatically maps real C FFT implementations to API‑driven FFT accelerators by resolving four concrete mismatches: code… | ||
| Business Meeting - PLDI 2022 | Jens Palsberg, Nate Foster, Roopsha Samanta, Rupak Majumdar | 01h 10m |
PLDI 2022 reports concrete process changes: a single flat PC of 120 with four area chairs, no full PC meeting, and asynchronous discussion; paper assignment… | ||
| Can Reactive Synthesis and Syntax-Guided Synthesis Be Friends? | Ruzica Piskac, Sanjana V. Suresh, Arjun Radhakrishnan | 18m |
Combines SyGuS for data-heavy fragments with temporal stream logic (TSL) reactive synthesis for control: SyGuS synthesizes pure functions (e.g., add1 then add1… | ||
| Certified Mergeable Replicated Data Types | Simon Fowler, Shin-Cheng Mu, Dmitriy Traytel | 18m |
A certified MRDT library implemented in F provides machine-checked specifications and proofs that three-way merge implementations preserve intents like… | ||
| Checking Robustness to Weak Persistency Models | Alastair Reid, Muralidhar Talagala, Karthikeyan Bhargavan | 19m |
PSign dynamically checks whether a program running under the x86 weak persistency model behaves as if it ran under strict persistency by constructing… | ||
| Choosing Mathematical Function Implementations for Speed and Accuracy | Stefan Marr, Klaus Ostermann | 19m |
A tool named optuner selects among 45 cosine and 49 sine implementations (about 4.8 million configurations) by building a linear error model from Taylor… | ||
| Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic | Aquiles Caro, Azadeh Farzan, Connor McBride | 19m |
Compass is a framework that gives strong, compositional specifications for relaxed-memory libraries by combining logical atomicity with partial-order… | ||
| Computing Correctly with Inductive Relations | Lennart Beringer, Cătălin Hriţcu | 20m |
Tool automatically derives semi-decision enumerators and checkers from inductive relations in Coq, using Ltac2 meta-programming to emit decision procedures… | ||
| CycleQ: an efficient basis for cyclic equational reasoning | Andreas Abel, Frédéric Blanqui | 15m |
CycleQ presents a cyclic proof system that folds equational reasoning into cycle formation via a synthesized subst rule, implemented as a Haskell GHC plugin… | ||
| Deep and Shallow Types for Gradual Languages | Jeremy G. Siek, Max S. New, Michael M. Vitousek | 18m |
Combines deep (natural) and shallow (transient) gradual typing into one language and proves they interoperate while preserving deep’s type soundness and… | ||
| Deoptless: Speculation with Dispatched On-Stack Replacement and Specialized Continuations | Maxime Chevalier Boisvert, Laurent Dufour, Maziar Gholami | 16m |
Deoptless claims to avoid costly deoptimizations by compiling specialized continuations at OSR points and using context dispatch to pick among them, so… | ||
| Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris | Cédric Fournet, Luca Padovani | 18m |
Built on Iris, Diaframe provides a foundational yet automated verifier for fine‑grained concurrency, using syntax‑directed rule versions, goal‑directed proof… | ||
| Differential Cost Analysis with Simultaneous Potentials and Anti-potentials | Viktor Vafeiadis, Nikolaj Bjørner | 17m |
A prototype automatically synthesizes simultaneous potentials and anti-potentials as polynomial templates, translates the universal polynomial constraints via… | ||
| DISTAL: The Distributed Tensor Algebra Compiler | Arjun Radhakrishnan, Stuart R. A. Jones, William F. Godoy | 19m |
DISTAL is a compiler that takes tensor index notation plus a tensor distribution notation and a scheduling language with distribute/communicate/rotate to emit… | ||
| Efficient Approximations for Cache-conscious Data Placement | Daniel Lustig, Gianluca Palermo | 17m |
Shows a linear-time 1+ε approximation for minimizing cache misses in direct-mapped caches under a sparsity assumption on the access graph, reducing placement… | ||
| Exocompilation for Productive Programming of Hardware Accelerators | Rohit B. Nair, Paul Vines | 20m |
Exocompilation presents a small imperative array DSL embedded in Python that generates C, models accelerator ops (load, mapmo, store) as subprocedures, and… | ||
| Finding Typing Compiler Bugs | Ewan K. Tempero, Viktor Vafeiadis | 18m |
Ephesus builds a program generator that emits large (500–1000 line) polymorphic programs and two transformation tests: type erasure mutation removes optional… | ||
| Formally Verified Lifting of C-compiled x86-64 Binaries | Simon L. Peyton Jones, Glynn Winskel | 19m |
A disassembler is built that lifts C‑compiled x86‑64 binaries into horograph outputs: graphs whose edges are Hoare triples and whose nodes are state… | ||
| FreeTensor: A Free-form DSL with Holistic Optimizations for Irregular Tensor Programs | Yuan Tang, Jack W. Davidson | 16m |
A Python-embedded DSL and compiler that compiles loop-based, irregular tensor code to native CPU/GPU kernels, using polyhedral analysis via isl to enable legal… | ||
| All you need is Superword-Level Parallelism: Systematic Control-Flow Vectorization with SLP | Chris Lattner, Michael I. Gordon | 17m |
This work generalizes SLP vectorization to pack independent, isomorphic instructions across different control-flow regions by converting code to predicated SSA… | ||
| Guaranteed bounds for posterior inference in universal probabilistic programming | Anders Sandberg, Apostolos Syropoulos | 18m |
Provides guaranteed numeric bounds on posterior probabilities by partitioning trace space into interval traces and using interval arithmetic to bound… | ||
| Hamband: RDMA Replicated Data Types | Ali Ghodsi, Matei Zaharia | 18m |
First hybrid replicated data types for RDMA that implement synchronization groups (strongly connected components of a conflict graph) with a single-leader… | ||
| Hardening Attack Surfaces with Formally Proven Binary Format Parsers | Aseem Rastogi, Ryan F. Kelly | 18m |
A toolchain converts a descriptive 3D format into F proofs and then to C, yielding memory- and integer-safe parsers with functional correctness and… | ||
| Getting Your Research Adopted | Margo Seltzer | 55m |
Advice focuses on concrete tactics: embed yourself via internships or sabbaticals, publish code and data on GitHub with a usable README, and build real systems… | ||
| Imposter Syndrome, Stupid Questions, and Eight (+/-2) Problems I Need your Help With | Aditya V. Nori | 52m |
Claims that many ML papers have algorithm and implementation mismatches and that bugs can make broken methods appear to work; demonstrates an optimal sparse… | ||
| Interpreter-guided Differential JIT Compiler Unit Testing | Andreas Zeller, Ondřej Lhoták | 19m |
Interpreter-guided concolic testing uses the VM interpreter as executable semantics to auto-generate unit tests for JIT-compiled code, modeling… | ||
| IRDL: An IR Definition Language for SSA Compilers | Chris Lattner, John Regehr | 17m |
A compact declarative language and toolchain that generates MLIR dialect bindings as C++/tablegen or supports runtime registration, applied to the MLIR… | ||
| Islaris: Verification of Machine Code Against Authoritative ISA Semantics | Nate Foster, Jan Newmarch | 18m |
Islaris verifies machine code against authoritative ISA mechanizations by pruning huge Sail models with SMT-backed Isla symbolic execution into compact Isla… | ||
| Karp: A Language for NP Reductions | Stephen A. Cook, David S. Johnson | 22m |
Karp is a domain-specific language that encodes NP reductions as runnable programs, derives problem solvers by translating verifiers to Rosette for symbolic… | ||
| Kleene Algebra Modulo Theories: A Framework for Concrete KATs | Katherine Gray | 17m |
Framework that turns a KAT into a concrete, decidable KAT when you supply three things: primitive actions/tests with weakest preconditions, sound/complete… | ||
| Landmarks and Regions: A Robust Approach to Data Extraction | Arjun R. Srinivasan, Suman K. Addepalli, Senanu Osei-Bryson | 19m |
Introduces a landmark-and-region synthesis pipeline that narrows extraction to small ROIs derived from nearby invariant strings, then runs lightweight programs… | ||
| Lasagne: A Static Binary Translator for Weak Memory Model Architectures | Alexandru Gheorghiu, Viktor Vafeiadis, Luca Botti | 17m |
Lasagne is a static x86→ARM translator that lifts x86 binaries to LLVM IR (via Microsoft mactool), applies pattern-based IR refinements to recover pointer… | ||
| Leapfrog: Certified Equivalence for Protocol Parsers | Boyi Xie, Rafael Rojas, Toby Murray | 17m |
Leapfrog proves that a high-level P4 parser and its optimized target automaton recognize the same packet language by modeling parsers as finite automata, using… | ||
| Low-Latency, High-Throughput Garbage Collection | Antony L. Hosking, Philipp H"olzenspies | 19m |
Implements a new collector called alexa (xr/rxi) on JDK 11 with mntk and claims simultaneous low tail latency and high throughput by combining reference… | ||
| Mako: A Low-Pause, High-Throughput Evacuating Collector for Memory-Disaggregated Datacenters | Ryan Stutsman, Sriram Rao | 17m |
Mako is an evacuating collector that offloads GC work to memory servers in RDMA‑connected, memory‑disaggregated datacenters, using a heap indirection table… | ||
| Modular Information Flow Through Ownership | Ahmad-Reza Sadeghi | 22m |
Repurposes Rust ownership and lifetimes to give a modular, static information flow analysis that requires no extra annotations, with a formal soundness proof… | ||
| Odin: On-Demand Instrumentation with On-the-Fly Recompilation | Justin Tolentino | 19m |
Odin implements on-demand instrumentation plus on-the-fly recompilation over compiler IR, partitioning programs into optimization-aware fragments and… | ||
| P4BID: Information Flow Control in P4 | Andrew Baumann | 21m |
Tool implements an information-flow type system for P4 as a static type checker built on the P4 reference compiler, flags table-based leaks that arise when… | ||
| PDL: A High-Level Hardware Design Language for Pipelined Processors | Andrew T. Campbell | 19m |
PDL is a domain-specific language that compiles high-level, one-instruction-at-a-time semantics into pipelined hardware by emitting RTL and checking… | ||
| Progressive Polynomial Approximations for Fast Correctly Rounded Math Libraries | Bruno Grenier, Sylvain Guilley | 19m |
Paper presents a Clarkson‑inspired, fast randomized LP solver that samples and reweights constraints to solve low‑dimensional linear programs with billions of… | ||
| PyLSE: A Pulse-Transfer Level Language for Superconductor Electronics | Michael P. Frank | 18m |
A Python DSL called PyLSE lets designers write pulse-based superconducting circuits as pulse machines with explicit setup/hold and propagation delays, a… | ||
| Quartz: Superoptimization of Quantum Circuits | Anna Aleksandrova, Nadav Zilberstein | 19m |
Quartz automatically generates and formally verifies symbolic circuit transformations and uses a cost-based backtracking optimizer to reduce quantum circuits… | ||
| Quickstrom: Property-based acceptance testing with LTL specifications | Simon Fowler, Gavin Bierman | 20m |
Quickstrom brings property-based testing to WebDriver acceptance tests by running generated action sequences against a web UI and checking LTL specifications… | ||
| Recursion Synthesis with Unrealizability Witnesses | Leonardo de Moura, Michael Emmi | 18m |
Procedure synthesizes recursive functions by combining syntax-guided synthesis with a new functional unrealizability checker that emits counterexample… | ||
| Relational Compilation for Performance-Critical Applications | Sébastien Chassignet, Koushik Sen | 21m |
Claims a proof-producing toolkit (Rupicola) that compiles specific high-level functional programs into low-level imperative code by proving "there exists"… | ||
| Response to “Synthesizing Input Grammars”: A Replication Study | Murad A. Rakhimov, Claire Le Goues | 08m |
Replication reimplementation uses a different codebase and evaluation pipeline and reports F1 scores lower than paper but still shows Glade outperforming L-… | ||
| RunTime-Assisted Convergence in Replicated Data Types | Kashyap Thadani | 18m |
Presents Quark, a runtime that enforces convergence for mergeable replicated data types by delaying merges (not edits) so arbitrary merge functions and… | ||
| RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code | Niki Vazou, Ranjit Jhala | 19m |
RustHornBelt gives a formal, mechanized bridge between RustHorn-style automatic specs and RustBelt’s unsafe-code semantics: a Coq model built on Iris… | ||
| Semantic Soundness for Language Interoperability | Robert L. Seidl | 20m |
Proves that linking heterogeneous languages is sound by building realizability models over a common untyped target and reasoning about the actual glue code… | ||
| Sequential Reasoning for Optimizing Compilers Under Weak Memory Concurrency | Mark Batty, Alastair F. Donaldson | 18m |
Claim: a new sequential semantics seq suffices to prove compiler optimizations sound even when linked into arbitrary weak‑memory contexts modeled by the… | ||
| Software-Hardware Codesign for Efficient In-Memory Regular Pattern Matching | Mikko Lipasti | 19m |
Provides a conservative static analysis that labels counted regex regions as easy (single-register) or ambiguous (needs per-state vector), compiles regexes… | ||
| Sound Sequentialization for Concurrent Program Verification | Alexey Gotsman, Thomas A. Henzinger | 18m |
Transforms concurrent code into a sequential program via sound sequentialization that picks one representative per commutativity equivalence class using… | ||
| Synthesizing Analytical SQL Queries from Computation Demonstration | Sanjay Rawat, Tova Milo | 17m |
Proposes a new specification called computation demonstration where users provide cell‑level expressions and optional ellipses instead of only final values… | ||
| “Synthesizing Input Grammars”: A Replication Study | Jonathan Bell, Rishabh Singh | 17m |
Replication reimplements the PLDI 2017 GLADE algorithm and finds its published claims don’t hold up: the provided replication packages use a custom serialized… | ||
| Is it Time to Retire Manual Concurrent Memory Reclamation? | Maged M. Michael | 15m |
Presents a concrete recipe to convert manual SMR into concurrent reference counting, turning hazard pointers, EBR and hybrid schemes into RC variants… | ||
| TF-Coder: Program Synthesis for Tensor Manipulations | Adam Lerer, Eugene Brevdo | 19m |
TF‑Coder turns an input/output example plus optional text into a TensorFlow expression by enumerative search that uses weighted search and operation filtering… | ||
| Verifying Optimizations of Concurrent Programs in the Promising Semantics | Shayan Nassirpour | 18m |
Verifies that common compiler passes preserve behavior under promising semantics 2.1 by defining a thread-local simulation plus a non-preemptive semantics to… | ||
| Visualization Question Answering Using Introspective Program Synthesis | Kuan-Ting Chen, Lisa Anne Hendricks | 19m |
POLL refines a VQA model’s noisy outputs by synthesizing executable explanation programs: a top-down abstract synthesis stage emits partial programs and a… | ||
| WARio: Efficient Code Generation for Intermittent Computing | Yi-Min Wang, Tianyu Zhao | 18m |
WARio builds a compiler pass that cuts required checkpoints by clustering write-after-read sites and grouping loop stores, using the Noel LLVM framework plus… | ||
| Warping Cache Simulation of Polyhedral Programs | CANBERK MUTLU, JAN REINEKE | 23m |
A simulation system builds a Presburger polyhedral trace of looped, input‑independent programs, runs a plug‑in cache simulator and a warp component that… | ||
| WebRobot: Web Robotic Process Automation using Interactive Programming-by-Demonstration | Rui Dong, Zhicheng Huang, Ian Iong Lam, Yan Chen, Xinyu Wang | 19m |
WebRobot is an interactive programming-by-demonstration tool for web RPA that synthesizes automation programs by speculation-and-validation instead of heavy… | ||
| Welcome to | ranjeet jhala | 04m |
Conference opens with logistics and a packed program: 70 live talks and an additional 72 virtual talks curated into a SIGPLAN track, plus two keynotes. Lunches… | ||
| nothing matches | ||