PLDI 2026
2026-06-15..2026-06-19
Boulder, 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 47th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2026)! 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 2026 will be held in person at the Limelight Boulder in Boulder, Colorado, USA. The main PLDI conference will be held from Wednesday, June 17, through Friday, June 19. Workshops and tutorials were held on Monday, June 15, and Tuesday, June 16. Registration opens on Monday, March 16, 2 ...
who it's for
programming language researchers, compiler engineers, formal verification researchers, GPU compiler engineers, language implementers, tool and infrastructure engineers, quantum compiler engineers
topics
advanced operator fusion for GPUs; SIMT subgroup operational semantics; simulator-based leakage proofs; preprocessor-aware C-to-Rust translation; versioned e-graphs and equality saturation; block-encoding quantum compilation; denotation-based compositional compiler verification; atomicity monitoring algorithms; Rust-style borrowing on GHC; streaming BPE tokenization algorithm; supermartingales for probabilistic verification; trace-guided synthesis of test generators
| title | author | length |
|---|---|---|
| Pantomime: Constructive Leakage Proofs via Simulation | Robin Webbers, Robert Schenck, Wind Wong, Kristina Sojakova, Klaus von Gleissenthall | 20m |
Claims a constructive alternative to non-interference: build a simulator circuit that reproduces all attacker-observable timing using only the censored secret… | ||
| Hayroll: A Modular Wrapper for Translating C Macros and Conditional Compilation to Rust | Haoran Peng, Baris Kasikci, Gilbert Louis Bernstein, Michael D. Ernst | 20m |
Hayroll is a modular wrapper that makes C-to-Rust translators preprocessor-aware without changing them by splitting work into a conditional-compilation layer… | ||
| Neptune: Advanced ML Operator Fusion for Locality and Parallelism on GPUs | Yifan Zhao, Egan Johnson, Prasanth Chatarasi, Vikram S. Adve, Sasa Misailovic | 18m |
Neptune is a tensor compiler that implements advanced operator fusion by deliberately breaking loop-carried dependencies and synthesizing algebraic repair… | ||
| Pure Borrow: Linear Haskell Meets Rust-Style Borrowing | Yusuke Matsushita, Hiromi Ishii | 19m |
Pure Borrow implements Rust-style borrowing as a Linear Haskell library that runs on GHC, exposing a BO monad for lifetime-restricted mutation… | ||
| Fast Atomicity Monitoring | Hünkar Can Tunç, Yifan Dong, Andreas Pavlogiannis | 16m |
Presents AtomSanitizer, an algorithm for conflict serializability that reduces worst-case time to O(nk^2) by tracking approximate latest-remote and… | ||
| Equality Saturation for Quantum Circuit Optimization | Ganxiang Yang, Paige Raun, Runzhou Tao, Ronghui Gu | 19m |
Quasar builds a compiler pass that constructs two complementary e-graphs (graph and sequence views), infers a compact 40 atomic rewrites set from thousands… | ||
| Intrinsically Correct Algorithms and Recursive Coalgebras | Cass Alexandru, Henning Urbat, Thorsten Wißmann | 21m |
Presents a new sufficient criterion: functors on families indexed by a well-founded relation that factor through restriction are well-founded functors, and… | ||
| State Space Estimation for DPOR-Based Model Checkers | A. R. Balasubramanian, Mohammad Hossein Khoshechin Jorshari, Rupak Majumdar, Umang Mathur, Minjian Zhang | 19m |
Proves counting Mazurkiewicz classes is #P-hard and inapproximable, then builds a polynomial‑time Monte Carlo estimator by turning an optimal stateless DPOR… | ||
| SIMT-Step Execution: A Flexible Operational Semantics For GPU Subgroup Behavior | Zheyuan Chen, Naomi Rehman, Guido Martínez, Tyler Sorensen | 19m |
Formal operational semantics defines subgroup behavior using dynamic basic blocks and a spectrum classifying instructions as independent, synchronous, or… | ||
| An Efficient Algorithm for Streaming BPE Tokenization | Konstantinos Mamouras, Angela W. Li, Yudi Yang | 20m |
Claims a linear-time, low‑memory streaming algorithm for BPE tokenization that reads input in blocks sized by a rule‑set dependent delay and emits safe… | ||
| Cobble: Compiling Block Encodings for Quantum Computational Linear Algebra | Charles Yuan | 21m |
Cobble compiles high-level matrix expressions into correct quantum circuits by representing matrices as block encodings, computing time and space costs… | ||
| MatchBox: A Semantic Foundation for Data Plane Portability | Eric Hayden Campbell, Robert Zhang, Divyanshu Saxena, Aditya Akella, Işıl Dillig | 20m |
MatchBox provides a provable translation pipeline that turns source match-action tables into compact, semantically equivalent target tables using a new… | ||
| SAIL: Sound Abstract Interpreters with LLMs | Qiuhan Gu, Avaljot Singh, Gagandeep Singh | 22m |
Framework uses LLMs to synthesize globally sound abstract transformers by casting synthesis as a constrained optimization problem with a principled cost… | ||
| Analyzing Bytes: Pre-Disassembly Static Binary Analysis | Huan Nguyen, Soumyakant Priyadarshan, Chencheng Jiang, R. Sekar | 18m |
Built a pre-disassembly analyzer (AMaze) that runs a backward dataflow on an super-set control-flow graph that treats every byte offset as a potential… | ||
| A Hierarchy of Supermartingales for ω-Regular Verification | Satoshi Kura, Hiroshi Unno | 20m |
Defines four new certificate classes and proves a strict hierarchy: GSSMs complete for positive recurrence, DVSSMs complete for null recurrence and the most… | ||
| Verification Modulo Tested Library Contracts | Abhishek Uppar, Omar Muhammad, Sumanth Prabhu S, Deepak D'Souza, P. Madhusudan, Adithya Murali | 22m |
Proposes a concrete pipeline that synthesizes method contracts and loop invariants by looping a generalizing CHC solver (ICE learners, decision trees, optional… | ||
| Parameterized Algorithms and Complexity for Function Merging with Branch Reordering | Amir Kafshdar Goharshady, Kerim Kochekov, Tian Shu, Ahmed Khaled Zaher | 18m |
Shows that allowing function merging with branch reordering makes the optimization NP-hard, then gives parameterized algorithms: a constructive FPT algorithm… | ||
| Scalable Floating-Point Satisfiability via Staged Optimization | Yuanzhuo Zhang, Zhoulai Fu, Binoy Ravindran | 18m |
StageSAT reframes floating-point SAT as three optimization stages: a fast projection-aided square residuals descent to find a trustworthy basin, a bit-precise… | ||
| Expecto: Extracting Formal Specifications from Natural Language Description for(…) | Dongjae Lee, Kihong Heo | 21m |
Expecto converts natural language intents into a concise DSL and uses a neuro-symbolic pipeline with GPT-4.1 Mini for synthesis and Z3 for validation, building… | ||
| Navigating AND–OR Graph Modifications to Debug Failing Proof Search | Justin Lubin, Marlena Preigh, Max Willsey, Sarah E. Chasins | 18m |
Provides a concrete debugging method that navigates modifications to AND–OR graphs rather than the raw graph, implemented by compiling modification constraints… | ||
| Trace-Guided Synthesis of Effectful Test Generators | Zhe Zhou, Ankush Desai, Benjamin Delaware, Suresh Jagannathan | 21m |
Underapproximate type-and-effect specs (U-hats) plus a small typed DSL synthesize effectful test generators that interact with black-box systems rather than… | ||
| Optimal Predicate Pushdown Synthesis | Robert Zhang, Eric Hayden Campbell, Dixin Tang, Işıl Dillig | 17m |
Systematically moves filters through stateful fold-based UDFs by synthesizing the strongest pre-filter Q and weakest residual P' that preserve semantics via a… | ||
| Homomorphism Calculus for User-Defined Aggregations | Ziteng Wang, Ruijie Fang, Linus Zheng, Dixin Tang, Işıl Dillig | 19m |
Introduces a decidable homomorphism calculus and a synthesis tool Inc that reduces dataframe homomorphism verification to a local per-row check via a… | ||
| Compiling to Recurrent Neurons | Joey Velez-Ginorio, Nada Amin, Konrad Kording, Steve Zdancewic | 18m |
Defines a linearly typed higher-order language Cajal(N) that compiles iteration and conditionals into matrices realized as recurrent neurons, proves a compiler… | ||
| Cerisier: A Program Logic for Attestation in a Capability Machine | June Rousseau, Denis Carnier, Thomas Van Strydonck, Steven Keuchel, Dominique Devriese, Lars Birkedal | 16m |
Cerisier presents a program logic that formalizes CHERI-TrEE support for enclaves on a capability machine and claims modular, end-to-end proofs for systems… | ||
| Revisiting Partial Tracing for Safe, Efficient, and Concurrent Garbage Collection in(…) | Jeonghyeon Kim, Jongse Park, Youngjin Kwon, Jeehoon Kang | 20m |
Implements a library-quality concurrent GC for unmanaged languages that keeps precise reference-counted roots and traces the heap, using phase consensus and a… | ||
| Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic | Guido Martínez, Bastian Köpcke, Jonáš Fiala, Gabriel Ebner, Tahina Ramananandro, Michel Steuwer, Tyler Sorensen, Nikhil Swamy | 21m |
Kuiper is an F library that uses Pulse-based separation logic to verify GPU kernels, extending the logic with forall+ connective and located resources to model… | ||
| Project Everest: Perspectives from Developing Industrial-Grade High-Assurance(…) | Danel Ahman, Karthikeyan Bhargavan, Barry Bond, Jay Bosamiya, Christopher Brzuska, Antoine Delignat-Lavaud, Cédric Fournet, Aymeric Fromherz, Sydney Gibson, Chris Hawblitzel, Cătălin Hriţcu, Markulf Kohlweiss, Guido Martínez, Haobin Ni, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Exequiel Rivas, Nikhil Swamy, Santiago Zanella-Béguelin | 23m |
Project Everest produces a verified TLS stack and crypto suite rather than promises: it yields 1.3 million lines of F source that build in two hours, emits… | ||
| Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation(…) | Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen, Kwing Hei Li, Joseph Tassarotti, Lars Birkedal | 21m |
Claims a program logic that encodes privacy budget as resource inside a probabilistic higher-order separation logic, proves an adequacy theorem linking the… | ||
| Flow-Analysis-Based Closure Optimization | John Reppy, Olin Shivers, Byron Zhong | 21m |
Implementation in Standard ML of New Jersey with an LLVM backend uses a sparse zero-CFA to guide concrete closure-representation decisions: selective heap… | ||
| Weighted NetKAT: A Programming Language For Quantitative Network Verification | Emmanuel Suárez Acevedo, Tiago Ferreira, Kevin Batz, Oliver Bøving, Nate Foster, Alexandra Silva | 20m |
Weighted NetKAT extends NetKAT to be parametric on a semiring and provides both denotational and operational semantics plus a compiler that turns programs into… | ||
| Hybrid Path-Sums for Hybrid Quantum Programs | Christophe Chareton, Jad Issa, Mathieu Nguyen, Nicolas Blanco, Sébastien Bardin | 18m |
Presents a formalism called Hybrid Path-Sums (HPS), a symbolic representation plus rewriting rules and a core assertion language, and ships a working symbolic… | ||
| Fungible Memories for Automated Technology Mapping and Retargeting | Zachary D. Sisco, Sijie Kong, Daniel Ruelas-Petrisko, Jingtao Xia, Julian Springer, Varun Rao, Spencer Wang, Gus Henry Smith, Ben Hardekopf, Jonathan Balkind | 22m |
Memo implements a write-once, map-anywhere memory abstraction that automatically retargets memories across simulation, FPGA and ASIC backends, and lifts… | ||
| The Rise & Collapse of a Quantum State | Aws Albarghouthi | 01h 10m |
Describes a practical pipeline: rewrite-rule synthesizer converts small peephole circuits into algebraic polynomials and uses a randomized Schwarz–Zippel check… | ||
| Virtualizing Continuations | Cong Ma, Jonghyun Jung, Yizhou Zhang | 21m |
Implements a novel virtual continuation scheme that assigns virtual addresses to stack-allocated handlers and mediates effect invocations via a software MMU… | ||
| GradInf: Gradient Estimation as Probabilistic Inference | Gaurav Arya, Mathieu Huot, Moritz Schauer, Alexander K. Lew, Feras A. Saad | 19m |
Introduces GradInf, a source-to-source system that reduces gradient-of-expectation problems to probabilistic inference by synthesizing an inference target via… | ||
| Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for(…) | Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao, Tiark Rompf | 18m |
Presents an algorithmic design for reachability types that proves sound and decidable bidirectional typing and avoidance, mechanized in Lean 4 and accompanied… | ||
| Probabilistic Refinement Session Types | Qiancheng Fu, Ankush Das, Marco Gaboardi | 23m |
Introduces probabilistic refinement session types and implements a prototype PReST prototype in OCaml with a bi-directional type checker that emits nonlinear… | ||
| Syntactic Implicit Parameters with Static Overloading | Daan Leijen, Tim Whiting | 20m |
Presents a simple, orthogonal design that combines syntactic implicit parameters and static overloading, formalizes coherence and gives a sound, complete… | ||
| Modular GPU Programming with Typed Perspectives | Manya Bansal, Daniel Sainati, Joseph W. Cutler, Saman Amarasinghe, Jonathan Ragan-Kelley | 20m |
Prism is a low-level GPU language that tracks thread32 perspective and other granularities in types, exposes constructs like split and group and partition… | ||
| The Downgrading Semantics of Memory Safety | René Rydhof Hansen, Andreas Stenbæk Larsen, Aslan Askarov | 20m |
Proposes gradual allocator independence: a semantic property saying program traces must not distinguish allocator implementations except where explicitly… | ||
| Active Learning for Neurosymbolic Program Synthesis | Celeste Barnaby, Jocelyn Qiaochu Chen, Ramya Ramalingam, Osbert Bastani, Işıl Dillig | 18m |
Proposes a concrete active-learning pipeline for neurosymbolic synthesis that models neural uncertainty with constrained conformal evaluation and avoids… | ||
| Implementability of Global Distributed Protocols Modulo Network Architectures | Elaine Li, Thomas Wies | 20m |
This work gives a precise, network-parametric characterization of when a bird’s-eye global message protocol admits a distributed implementation: coherence… | ||
| SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum(…) | Nengkun Yu, Jens Palsberg, Thomas Reps | 18m |
SAQR-QC combines quantum Hoare-style inequalities with quantum abstract interpretation to trade exactness for speed: each reasoning step touches only local… | ||
| StreamAlloc: A Framework for Analyzing and Transforming CUDA Code to Enable(…) | Soumik Kumar Basu, Jyothi Vedurada | 20m |
StreamAlloc implements sync2async as a compiler pass using LLVM/Clang to convert synchronous cudaMemcpy and kernel launches into async calls with automatically… | ||
| Cpp2Rust: Automatic Translation of C++ to Safe Rust | Lucian Popescu, Francisco Gouveia, Henrique Preto, João Silveira, Dmytro Hrybenko, José Fragoso Santos, Nuno P. Lopes | 19m |
Cpp2Rust automatically translates arbitrary C++ into memory-safe Rust by representing locals as Rc<RefCell<T>>-backed values and pointers as weak PTR handles… | ||
| Choose, Don’t Label: Multiple-Choice Query Synthesis for Program Disambiguation | Celeste Barnaby, Danny Ding, Osbert Bastani, Işıl Dillig | 20m |
A new active-learning system called Socrates generates multiple-choice queries (each option a Hoare triple) instead of asking users to label concrete inputs… | ||
| CRIS: The Power of Imagination in Hybrid Verification | Yonghee Kim, Taeyoung Yoon, Sanghyun Yi, Jaehyung Lee, Soonwon Moon, Yeji Han, Seonho Lee, Taeyoung Rhee, Yujin Im, Donghyun Nam, Jieung Kim, Chung-Kil Hur | 19m |
Introduces CRIS, a framework that extends CCR with imaginary specifications—specs that intermix executable code and separation-logic assertions—to prove… | ||
| Denotation-based Compositional Compiler Verification | Zhang Cheng, Jiyang Wu, Di Wang, Qinxiang Cao | 17m |
Proposes a denotational framework that represents each statement by three behavior sets (normal, error, divergence) enriched with traces and distinguishes… | ||
| FlexHeap: Dynamic I/O-Aware Heap Resizing for Managed Applications | Iacovos G. Kolokasis, Shoaib Akram, Foivos S. Zakkak, Polyvios Pratikakis, Angelos Bilas | 18m |
FlexHeap is a G1 heap-resizing implementation in OpenJDK 21 G1 that measures GC lost cycles and per-mutator I/O stalls via eBPF sched_switch to repartition a… | ||
| Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics | Rui Dong, Qingyue Wu, Danny Ding, Zheng Guo, Ruyi Ji, Xinyu Wang | 19m |
Proposes offline presynthesis that builds a semantics tree automaton and a reachability oracle so online synthesis reduces to fast graph reachability queries… | ||
| Iris-WasmFX: Modular Reasoning for Wasm Stack Switching | Maxime Legoupil, Mathias Pedersen, Lars Birkedal, Sam Lindley, Jean Pichon-Pharabod | 19m |
Mechanisation in Rocq produces WasmFXCert and a syntactic type-safety proof for Wasm with explicit stack continuations, proving the extension sound… | ||
| Optimism in Equality Saturation | Russel Arbore, Alvin Cheung, Max Willsey | 24m |
Shows that a naive optimistic e-class analysis on e-graphs becomes unsound because rewrites create ill‑formed cycles that look like loops but aren’t, and… | ||
| Dynamically Checked Deep Immutability in Python | Fridtjof Peer Stoldt, Sylvan Clebsch, Matthew A. Johnson, Matthew J. Parkinson, Tobias Wrigstad | 19m |
Adds deep immutability to CPython 3.15 via 7,000 lines of runtime code, an atomic refcount for immutable objects, and write barriers inserted at 148 hot sites… | ||
| A Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs | Amanda Liu, Gilbert Louis Bernstein, Shoaib Kamil, Adam Chlipala, Jonathan Ragan-Kelley | 20m |
Mechanized framework extends ATL and uses the Rock proof assistant to produce a verified compression/decompression adjoint that rewrites dense tensor kernels… | ||
| Improving Equality Saturation for EDA via Semantic E-Graphs | Sijie Kong, Jingtao Xia, Daniel Ruelas-Petrisko, Zachary D. Sisco, Jonathan Balkind, Gus Henry Smith | 21m |
Introduces semantic e-graphs as an e-graph variant that encodes semantic IDs to link word- and bit-level hardware representations, and implements Nextmap, an… | ||
| A Formally Verified Foundation for Compositional Heterogeneous Coherence | An Qi Zhang, Andrés Goens, Daniel Sorin, Vijay Nagarajan | 17m |
Claims that the de-facto Principle of Synchronous Propagation is sufficient to guarantee the Compound Memory Consistency Model for a wide class of CPU/GPU… | ||
| Semantic Reification: A New Paradigm for Random Program Generation | Kavya Chopra, Cong Li, Thodoris Sotiropoulos, Zhendong Su | 20m |
Claims a new semantic reification method that synthesizes a program P, input I, and expected output O from a CFG skeleton and a chosen execution path… | ||
| SSA without Dominance for Higher-Order Programs | Roland Leißa, Johannes Max Griebler | 19m |
Dominance is replaced by a data-flow notion of free-variable nesting tree that applies to higher-order, scopeless IRs; nesting implies (but is strictly… | ||
| VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type(…) | Travis Hance, Laila Elbeheiry, Yusuke Matsushita, Derek Dreyer | 20m |
Paper proves a machine-checked soundness theorem for a Verus subset by formalizing Verus’s proof-oriented types and translating them into Rust Hornbill–style… | ||
| SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine(…) | Longfei Qiu, Jingqi Xiao, Ji-Yong Shin, Zhong Shao | 18m |
SureDistrib defines probabilistic IO automata in the Rocq proof assistant and proves composition lemmas that let an abstract underlay be replaced by an… | ||
| Incremental Computation for Efficient Programmable Inference in Probabilistic Programs | Fabian Zaiser, Jack Czenszak, Martin C. Rinard, Vikash K. Mansinghka, Alexander K. Lew | 19m |
Compiles probabilistic programs to deterministic density functions, then applies a compositional incrementalization based on the incremental lambda calculus… | ||
| Bonsai: Compiling Queries to Pruned Tree Traversals | Alexander J Root, Christophe Gyurgyik, Purvi Goel, Kayvon Fatahalian, Jonathan Ragan-Kelley, Andrew Adams, Fredrik Kjolstad | 21m |
Bonsai compiles high-level queries plus an annotated algebraic tree spec into C++ single-pass traversals that automatically generate always/maybe/never pruning… | ||
| Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation | Shaurya Gomber, Debangshu Banerjee, Gagandeep Singh | 20m |
Proposes a general, parametric transformer that outputs a space of sound outputs (constructed by UPOSE) and then searches it with a differentiable AGG gradient… | ||
| Fixed Parameter Tractable Linearizability Monitoring | Zheng Han Lee, Umang Mathur | 20m |
Claims that linearizability monitoring is fixed‑parameter tractable parameterized by number of processes k for stacks, queues, priority queues and maps, giving… | ||
| Causality and Semantic Separation | Anna Zhang, Qinglan Luo, London Bielicke, Eunice Jun, Adam Chlipala | 19m |
Claim: a new semantic separation notion exactly matches graph-theoretic d-separation, with a full mechanized proof mechanized in Rocq. Construction uses… | ||
| Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification | Satoshi Kura, Hiroshi Unno, Takeshi Tsukada | 21m |
Presents a concrete criterion that turns uniqueness of least fixed points into a usable lower-bound proof: existence of a U-ranking supermartingale plus a… | ||
| Towards Removing Undef Values from LLVM IR | Pedro Lobo, John McIver, George Mitenkov, Juneyoung Lee, Kirshanthan Sundararajah, Nuno P. Lopes | 20m |
LLVM adds a new byte type and a freezing load that let uninitialized memory become poison instead of undef, fixing raw-copy and bitfield miscompilations… | ||
| Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow | Zhengyao Lin, Yi Cai, Milijana Surbatovich | 17m |
Wavelet is a formally verified compiler that translates a capability-annotated imperative IR into asynchronous dataflow graphs, mechanized in Lean and checked… | ||
| Solvable Tuple Patterns and Their Applications to Program Verification | Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, Ryo Yoshinaka | 20m |
Introduces solvable tuple patterns (STPs) and conjunctive STPs as a representation for relations among sequences that are learnable from only positive samples… | ||
| Responsive Parallelism with Dynamic and First-Class Priorities | Marelle León, My Dinh, Stefan K. Muller | 16m |
Extends PriML to make priorities first class and dynamically changeable, adding a change command and typing each command with start/duration/end refinements… | ||
| Abstract Interpretation with Confidence | Yuanfeng Shi, Ziyue Jin, Xin Zhang | 20m |
Paper defines alarm confidence as the probability of local completeness: the chance that a sampled concrete program, drawn from the set consistent with a given… | ||
| Versioned E-Graphs | Jahrim Gabriele Cesario, George Zakhour, Pascal Weisenburger, Guido Salvaneschi | 23m |
Introduces versioned e-graphs that store multiple conditional equivalence sets in one structure, implements a versioned union-find with propagation and version… | ||
| &inator: Correct, Precise C-to-Rust Interface Translation | Victor Chen, Ayden Coughlin, Michael D. Bond | 19m |
&inator automatically produces Rust declarations for C top-levels by formulating semantic-equivalence and borrow-checking as SMT constraints and solving them… | ||
| Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…) | Zain K Aamer, Rini Banerjee, Hiroyuki Katsura, David Kaloper-Meršinjak, Dimitrios J. Economou, Kayvan Memarian, Dhruv C. Makwana, Neel Krishnaswami, Benjamin C. Pierce, Christopher Pulte, Peter Sewell | 17m |
Integrates CN separation logic into runtime checks, unit and SMT-based random generator testing, and final machine-checked proofs, all on the real-world PKVM… | ||
| Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy | Eden Frenkel, Kenneth L. McMillan, Oded Padon, Sharon Shoham | 19m |
Proposes a proof system that breaks a single complex inductive invariant into incremental steps and proves each rule sound, implemented as a checker in myvy… | ||
| EREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination | Ekaterina Zhuchko, Ian Erik Varatalu, Margus Veanes, Nikolaj Bjørner | 22m |
Introduces Extended Regular Expressions with Quantifiers (EREQ) that translate wMSO to a regex-like formalism via a linear-time translation and eliminate… | ||
| Compiling Strassen-like Matrix Multiplication Algorithms to Fast CUDA Kernels | Abhinav Jangda | 18m |
SubCuber compiles Strassen-like algorithms into CUDA by building the algorithm dependency graph, choosing tile-wise schedules, and applying recursion-aware… | ||
| Exploiting Sophisticated Static Analysis for Verilog | Qinlin Chen, Nairen Zhang, Jinpeng Wang, Jiacai Cui, Tian Tan, Xiaoxing Ma, Chang Xu, Jian Lu, Yue Li | 19m |
A Verilog static-analysis framework named THU provides a front end, IR, analysis manager and a suite of 40 analyses built on reusable fundamentals (bit-vector… | ||
| A Compiler for Fused Relational Operations on Multisets | James Dong, Fredrik Kjolstad | 16m |
A compiler lowers physical query plans into an abstract loop IR that fuses inner joins, left/right/full outer joins, non‑equi joins, set ops and multiset (bag)… | ||
| Scalable and Accurate Application-Level Crash-Consistency Testing(…) | Yile Gu, Ian Neal, Jiexiao Xu, Shaun Christopher Lee, Ayman Said, Musa Haydar, Jacob Van Geffen, Andrew Quinn, Baris Kasikci | 20m |
Implements representative testing as an update-behavior heuristic and builds Pathfinder to trace POSIX and MMIO executions, construct a persistent graph of… | ||
| A Deductive System for Contract Satisfaction Proofs | Arthur Correnson, Haoyi Zeng, Jana Hofmann | 17m |
Claims a sound-and-complete deductive system for relative bisimulation that characterizes relative trace equality via a nested coinductive–inductive fixpoint… | ||
| Happiness U-Curve: Navigating the AI Validation Bottleneck with Conformance Testing and(…) | Miryung Kim | 01h 07m |
Argues that validation — not generation — is the AI bottleneck and demonstrates a concrete dual-track approach: property-skeletons plus automated proof… | ||
| Counterexample-Guided Inference of Modular Specifications | William T. Hallahan, Ranjit Jhala, Ruzica Piskac | 22m |
A counterexample-guided algorithm automatically infers missing callee specifications so a modular verifier can prove a client function, parameterized by a… | ||
| Backwards-Compatible Row-Based Exceptions in ML | Simcha van Collem, Paulo Emílio de Vilhena, Robbert Krebbers | 18m |
Type system extends ML with row polymorphism and a new top row to make exception tracking backwards compatible, proving that unannotated code types as top-row… | ||
| Categorical Semantics of Probabilistic Symbolic Execution | John M. Li, Jack Czenszak, Steven Holtzen | 22m |
Builds a denotational universe where symbolic execution is a presheaf model and proves a single metatheorem: any definitional interpreter written in the… | ||
| Heterogeneous Dynamic Logic: Provability Modulo Program Theories | Samuel Teuber, Mattias Ulbrich, André Platzer, Bernhard Beckert | 19m |
Heterogeneous Dynamic Logic treats each program logic as a dynamic theory and gives two concrete operations: Lifting to add constructs (havoc, regular… | ||
| SuperDP: Differential Privacy Refutation via Supermartingales | Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Đorđe Žikelić | 20m |
Method claims automated, sound refutation of ε‑DP by searching for a pair of inputs and a nonnegative output function whose expectations violate the ε bound… | ||
| Contextual Refinement of Higher-Order Concurrent Probabilistic Programs | Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal | 21m |
Claims a new logic, Foxtrot, that proves contextual refinement for higher-order concurrent probabilistic programs and handles higher-order local state… | ||
| Typestate via Revocable Capabilities | Songlin Jia, Craig Liu, Siyuan He, Haotian Deng, Yuyan Bao, Tiark Rompf | 15m |
Presents a Scala 3 compiler extension (prototype in Stella) that implements flow-sensitive revocation, ties capabilities to objects via path-dependent… | ||
| Synthesizing Backward Error Bounds, Backward | Laura Zielinski, Justin Hsu | 19m |
Introduces a composable, general alpha-beta stability definition that covers all five primitive floating-point ops (including sqrt) and composes under program… | ||
| Hyper Separation Logic | Trayan Gospodinov, Peter Müller, Thibault Dardinier | 21m |
Introduces a logic that supports hyperproperties with arbitrary quantifier alternation over heap programs, proves soundness in Isabelle/HOL, and ships reusable… | ||
| SparseZETA: Intelligent Auto-tuner for Designing High-Performance SpMV Programs | Zhen Du, Ying Liu, Xionghui Chen, Yanbo Zhao, Xiaobing Feng, Huimin Cui, Jiajia Li | 17m |
SparseZETA generates SpMV kernels by predicting and applying sequences of 24 concrete operators (compress, row/column blocking, padding, mapping, reduction… | ||
| Probabilistic Inference for Datalog with Correlated Inputs | Jingbo Wang, Shashin Halalingaiah, Weiyi Chen, Chao Wang, Işıl Dillig | 21m |
A new Datalog extension called Praline implements probabilistic inference that accounts for arbitrary input correlations by reducing exact inference to a… | ||
| Uniformity Analysis in the WebGPU Shading Language | James Lee-Jones, John Wickerson, Alastair F. Donaldson | 18m |
Provides a rigorous operational semantics for TinyWGSL that defines barrier divergence, formalizes the WGSL uniformity rules, and proves soundness sketches… | ||
| Programming Language Design and Implementation for the Machine Learning Era: A Personal(…) | Saman Amarasinghe | 54m |
Machine learning actually changes compiler work in three concrete ways: ML augments heuristics (the 2003 Meta Optimization effort evolves priority functions… | ||
| A Categorical Basis for Robust Program Analysis | Zachary Kincaid, Shaowei Zhu | 22m |
A categorical framework characterizes robustness: programs and properties become concrete categories over a base of transformations, and robust analyses become… | ||
| Programming Language Design and Implementation for the Machine Learning Era: A Personal(…) | Saman Amarasinghe | 54m |
Machine learning already augments and sometimes outperforms handcrafted compiler components: meta optimization (2003) evolves priority functions and yields… | ||
| Decoupling Data Layouts from Bounding Volume Hierarchies | Christophe Gyurgyik, Alexander J Root, Fredrik Kjolstad | 19m |
Scion DSL and compiler separate BVH logical ADTs from physical memory layouts and automatically specialize traversal with destructor and constructor… | ||
| Persistent Iterators with Value Semantics | Yihe Li, Gregory J. Duck | 18m |
Proposes persistent iterators that snapshot containers so iterator operations return new versions, implemented as the LibFpp C++ library using a finger tree… | ||
| CoTenN: Constrained Optimization with Tensor Networks | Ritvik Sharma, Cheng Peng, Siddharth Dangwal, Sara Achour | 20m |
A constraint-first DSL and compiler pipeline converts discrete quantum constrained optimization problems into tensor networks: Masq DSL expresses hard… | ||
| Contextual Embeddings: Implementing Bound Variables through Instance Resolution | Samantha Frohlich, Jessica Foster, G. A. Kavvos, Meng Wang | 19m |
Introduces contextual embeddings: an embedding that preserves typing contexts and uses the host's type-class instance-resolution based index reconstruction to… | ||
| Diagramming Program Values by Spatial Refinement | Siddhartha Prasad, Michael Tu, Karan Kashyap, Tim Nelson, Shriram Krishnamurthi | 18m |
A declarative DSL called Spytial maps runtime value graphs to 2D layouts via constraint solving and produces interactive diagrams with enforced spatial rules… | ||
| nothing matches | ||