PLDI 2026
Proceedings of the ACM on Programming Languages, Volume 10, Number PLDI

Title Page

Article: pldi26foreword-fm000-p doi:

Sponsors

Article: pldi26foreword-fm003-p doi:

Editorial Message
Manu Sridharan
(University of California at Riverside, USA)

Publisher's Version Article: pldi26editorial-fm001-p doi:10.1145/3818664

FlexHeap: Dynamic I/O-Aware Heap Resizing for Managed Applications
Iacovos G. Kolokasis, Shoaib Akram, Foivos S. Zakkak, Polyvios Pratikakis, and Angelos Bilas
(Foundation for Research and Technology Hellas, Greece; University of Crete, Greece; Australian National University, Australia; Red Hat, Ireland)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p2-p doi:10.1145/3808247

Fast Atomicity Monitoring
Hünkar Can Tunç, Yifan Dong, and Andreas Pavlogiannis
(Uber, Netherlands; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p10-p doi:10.1145/3808248

Versioned E-Graphs
Jahrim Gabriele Cesario, George Zakhour, Pascal Weisenburger, and Guido Salvaneschi
(University of St. Gallen, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p12-p doi:10.1145/3808249

Towards Removing Undef Values from LLVM IR
Pedro Lobo, John McIver, George Mitenkov, Juneyoung Lee, Kirshanthan Sundararajah, and Nuno P. Lopes
(INESC-ID, Portugal; Instituto Superior Técnico - University of Lisbon, Portugal; Virginia Tech, USA; Aptos Labs, UK; AWS, USA)

Publisher's Version ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p14-p doi:10.1145/3808250

A Deductive System for Contract Satisfaction Proofs
Arthur Correnson, Haoyi Zeng, and Jana Hofmann
(CISPA Helmholtz Center for Information Security, Germany; Harvard University, USA; MPI-SP, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p15-p doi:10.1145/3808251

Path-Sensitive Abstract Interpretation for WCET Estimation
Shangshang Xiao, Mengxia Sun, Wei Zhang, Naijun Zhan, and Lei Ju
(Shandong University, China; Peking University, China; Zhongguancun Laboratory, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi26main-p17-p doi:10.1145/3808252

Decoupling Data Layouts from Bounding Volume Hierarchies
Christophe Gyurgyik, Alexander J Root, and Fredrik Kjolstad
(Stanford University, USA)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p19-p doi:10.1145/3808253

Equality Saturation for Quantum Circuit Optimization
Ganxiang Yang, Paige Raun, Runzhou Tao, and Ronghui Gu
(Columbia University, USA; University of Maryland, USA; CertiK, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p23-p doi:10.1145/3808254

Cobble: Compiling Block Encodings for Quantum Computational Linear Algebra
Charles Yuan
(University of Wisconsin-Madison, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p24-p doi:10.1145/3808255

Bonsai: Compiling Queries to Pruned Tree Traversals
Alexander J Root, Christophe Gyurgyik, Purvi Goel, Kayvon Fatahalian, Jonathan Ragan-Kelley, Andrew Adams, and Fredrik Kjolstad
(Stanford University, USA; Massachusetts Institute of Technology, USA; Adobe Research, USA)

Publisher's Version Published Artifact Artifacts Available ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p25-p doi:10.1145/3808256

A Hierarchy of Supermartingales for ω-Regular Verification
Satoshi Kura and Hiroshi Unno
(Waseda University, Japan; Tohoku University, Japan)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p28-p doi:10.1145/3808257

Solvable Tuple Patterns and Their Applications to Program Verification
Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, and Ryo Yoshinaka
(University of Tokyo, Japan; Tokyo University of Agriculture and Technology, Japan; Tohoku University, Japan)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi26main-p33-p doi:10.1145/3808258

Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
Yusuke Matsushita and Hiromi Ishii
(Kyoto University, Japan; JIJ, Japan)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p38-p doi:10.1145/3808259

The Downgrading Semantics of Memory Safety
René Rydhof Hansen, Andreas Stenbæk Larsen, and Aslan Askarov
(Aalborg University, Denmark; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p49-p doi:10.1145/3808260

A Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs
Amanda Liu, Gilbert Louis Bernstein, Shoaib Kamil, Adam Chlipala, and Jonathan Ragan-Kelley
(Massachusetts Institute of Technology, USA; University of Washington, USA; Adobe, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p53-p doi:10.1145/3808261

Flow-Analysis-Based Closure Optimization
John Reppy, Olin Shivers, and Byron Zhong
(University of Chicago, USA; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p54-p doi:10.1145/3808262

Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow
Zhengyao Lin, Yi Cai, and Milijana Surbatovich
(Carnegie Mellon University, USA; University of Maryland at College Park, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p56-p doi:10.1145/3808263

Trace-Guided Synthesis of Effectful Test Generators
Zhe Zhou, Ankush Desai, Benjamin Delaware, and Suresh Jagannathan
(Purdue University, USA; Snowflake, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p68-p doi:10.1145/3808264

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs
Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, and Lars Birkedal
(Aarhus University, Denmark; New York University, USA)

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

Cpp2Rust: Automatic Translation of C++ to Safe Rust
Lucian Popescu, Francisco Gouveia, Henrique Preto, João Silveira, Dmytro Hrybenko, José Fragoso Santos, and Nuno P. Lopes
(INESC-ID, Portugal; Instituto Superior Técnico - University of Lisbon, Portugal; Google, Germany)

Publisher's Version Article: pldi26main-p91-p doi:10.1145/3808266

Compiling Strassen-like Matrix Multiplication Algorithms to Fast CUDA Kernels
Abhinav Jangda
(Microsoft Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p97-p doi:10.1145/3808267

Semantic Reification: A New Paradigm for Random Program Generation
Kavya Chopra, Cong Li, Thodoris Sotiropoulos, and Zhendong Su
(ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p100-p doi:10.1145/3808268

Contextual Embeddings: Implementing Bound Variables through Instance Resolution
Samantha Frohlich, Jessica Foster, G. A. Kavvos, and Meng Wang
(University of Bristol, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p102-p doi:10.1145/3808269

&inator: Correct, Precise C-to-Rust Interface Translation
Victor Chen, Ayden Coughlin, and Michael D. Bond
(Ohio State University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p110-p doi:10.1145/3808270

Iris-WasmFX: Modular Reasoning for Wasm Stack Switching
Maxime Legoupil, Mathias Pedersen, Lars Birkedal, Sam Lindley, and Jean Pichon-Pharabod
(Nanyang Technological University, Singapore; Aarhus University, Denmark; University of Edinburgh, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p111-p doi:10.1145/3808271

CoTenN: Constrained Optimization with Tensor Networks
Ritvik Sharma, Cheng Peng, Siddharth Dangwal, and Sara Achour
(Stanford University, USA; SLAC National Accelerator Laboratory, USA; University of Chicago, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p126-p doi:10.1145/3808272

Verification of Recursively Defined Quantum Circuits
Mingsheng Ying and Zhicheng Zhang
(University of Technology Sydney, Australia)

Publisher's Version ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p130-p doi:10.1145/3808273

Causality and Semantic Separation
Anna Zhang, Qinglan Luo, London Bielicke, Eunice Jun, and Adam Chlipala
(Massachusetts Institute of Technology, USA; Wellesley College, USA; University of California at Los Angeles, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p135-p doi:10.1145/3808274

Diagramming Program Values by Spatial Refinement
Siddhartha Prasad, Michael Tu, Karan Kashyap, Tim Nelson, and Shriram Krishnamurthi
(Brown University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p141-p doi:10.1145/3808275

Hayroll: A Modular Wrapper for Translating C Macros and Conditional Compilation to Rust
Haoran Peng, Baris Kasikci, Gilbert Louis Bernstein, and Michael D. Ernst
(University of Washington, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p150-p doi:10.1145/3808276

MatchBox: A Semantic Foundation for Data Plane Portability
Eric Hayden Campbell, Robert Zhang, Divyanshu Saxena, Aditya Akella, and Işıl Dillig
(University of Texas at Austin, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p153-p doi:10.1145/3808277

Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows
Zain K Aamer, Rini Banerjee, Hiroyuki Katsura, David Kaloper-Meršinjak, Dimitrios J. Economou, Kayvan Memarian, Dhruv Makwana, Neel Krishnaswami, Benjamin C. Pierce, Christopher Pulte, and Peter Sewell
(University of Pennsylvania, USA; University of Cambridge, UK; University of Oxford, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p155-p doi:10.1145/3808278

Choose, Don’t Label: Multiple-Choice Query Synthesis for Program Disambiguation
Celeste Barnaby, Danny Ding, Osbert Bastani, and Işıl Dillig
(University of Texas at Austin, USA; University of Pennsylvania, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p161-p doi:10.1145/3808279

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, and Nikhil Swamy
(Microsoft Research, USA; TU Berlin, Germany; ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p173-p doi:10.1145/3808280

Towards Efficient Matching of Regexes with Backreferences using Register Set Automata
Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Jan Vašák, and Sabína Gulčíková
(Brno University of Technology, Czech Republic; Aalborg University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p181-p doi:10.1145/3808281

Parameterized Algorithms and Complexity for Function Merging with Branch Reordering
Amir K. Goharshady, Kerim Kochekov, Tian Shu, and Ahmed Khaled Zaher
(University of Oxford, UK; Hong Kong University of Science and Technology, Hong Kong)

Publisher's Version Article: pldi26main-p183-p doi:10.1145/3808282

A Compiler for Fused Relational Operations on Multisets
James Dong and Fredrik Kjolstad
(Stanford University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi26main-p219-p doi:10.1145/3808283

SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits
Nengkun Yu, Jens Palsberg, and Thomas Reps
(Stony Brook University, USA; University of California at Los Angeles, USA; University of Wisconsin-Madison, USA)

Publisher's Version Article: pldi26main-p228-p doi:10.1145/3808284

NEURA: A Unified and Retargetable Compilation Framework for Coarse-Grained Reconfigurable Architectures
Shangkun Li, Jinming Ge, Diyuan Tao, Zeyu Li, Jiawei Liang, Linfeng Du, Jiang Xu, Wei Zhang, and Cheng Tan
(Hong Kong University of Science and Technology, Hong Kong; Independent Researcher, China; Hong Kong University of Science and Technology, Guangzhou, China; Google, USA; Arizona State University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p234-p doi:10.1145/3808285

SSA without Dominance for Higher-Order Programs
Roland Leißa and Johannes Max Griebler
(University of Göttingen, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p239-p doi:10.1145/3808286

Cerisier: A Program Logic for Attestation in a Capability Machine
June Rousseau, Denis Carnier, Thomas Van Strydonck, Steven Keuchel, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; KU Leuven, Belgium; Fortanix, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p266-p doi:10.1145/3808287

Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics
Rui Dong, Qingyue Wu, Danny Ding, Zheng Guo, Ruyi Ji, and Xinyu Wang
(University of Michigan, USA; University of Texas at Austin, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p272-p doi:10.1145/3808288

Virtualizing Continuations
Cong Ma, Jonghyun Jung, and Yizhou Zhang
(University of Waterloo, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p273-p doi:10.1145/3808289

Modular GPU Programming with Typed Perspectives
Manya Bansal, Daniel Sainati, Joseph W. Cutler, Saman Amarasinghe, and Jonathan Ragan-Kelley
(Massachusetts Institute of Technology, USA; University of Pennsylvania, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p277-p doi:10.1145/3808290

State Space Estimation for DPOR-Based Model Checkers
A. R. Balasubramanian, Mohammad Hossein Khoshechin Jorshari, Rupak Majumdar, Umang Mathur, and Minjian Zhang
(MPI-SWS, Germany; National University of Singapore, Singapore; University of Illinois Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p279-p doi:10.1145/3808291

Analyzing Bytes: Pre-Disassembly Static Binary Analysis
Huan Nguyen, Soumyakant Priyadarshan, Chencheng Jiang, and R. Sekar
(Google, USA; Stony Brook University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p284-p doi:10.1145/3808292

SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine Protocols
Longfei Qiu, Jingqi Xiao, Ji-Yong Shin, and Zhong Shao
(Yale University, USA; University of Hong Kong, China; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p304-p doi:10.1145/3808293

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, and Jonathan Balkind
(Chinese University of Hong Kong, Shenzhen, China; University of California at Santa Barbara, USA; University of Washington, USA; TU Berlin, Germany; University of California at Berkeley, USA; Southmountain Research, USA)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p315-p doi:10.1145/3808294

Heterogeneous Dynamic Logic: Provability Modulo Program Theories
Samuel Teuber, Mattias Ulbrich, André Platzer, and Bernhard Beckert
(KIT, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p324-p doi:10.1145/3808295

SuperDP: Differential Privacy Refutation via Supermartingales
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, and Đorđe Žikelić
(IST Austria, Austria; Singapore Management University, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p328-p doi:10.1145/3808296

SIMT-Step Execution: A Flexible Operational Semantics for GPU Subgroup Behavior
Zheyuan Chen, Naomi Rehman, Guido Martínez, and Tyler Sorensen
(University of California at Santa Cruz, USA; University of California at Santa Barbara, USA; Microsoft Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p337-p doi:10.1145/3808297

Neptune: Advanced ML Operator Fusion for Locality and Parallelism on GPUs
Yifan Zhao, Egan Johnson, Prasanth Chatarasi, Vikram Adve, and Sasa Misailovic
(University of Illinois Urbana-Champaign, USA; IBM Research, USA)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p347-p doi:10.1145/3808298

Improving Equality Saturation for EDA via Semantic E-Graphs
Sijie Kong, Jingtao Xia, Daniel Ruelas-Petrisko, Zachary D. Sisco, Jonathan Balkind, and Gus Henry Smith
(University of California at Santa Barbara, USA; University of Washington, USA; Chinese University of Hong Kong, Shenzhen, China; Southmountain Research, USA)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p348-p doi:10.1145/3808299

Exploiting Sophisticated Static Analysis for Verilog
Qinlin Chen, Nairen Zhang, Jinpeng Wang, Jiacai Cui, Tian Tan, Xiaoxing Ma, Chang Xu, Jian Lu, and Yue Li
(Nanjing University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p362-p doi:10.1145/3808300

Bridging Coverage and Confidence: Reliable Static False Alarm Elimination via Input-Agnosticity
Jiayi Wang, Yu Wang, Linzhang Wang, and Ke Wang
(Nanjing University, China)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p363-p doi:10.1145/3808301

Optimism in Equality Saturation
Russel Arbore, Alvin Cheung, and Max Willsey
(University of California at Berkeley, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p376-p doi:10.1145/3808302

Backwards-Compatible Row-Based Exceptions in ML
Simcha van Collem, Paulo Emílio de Vilhena, and Robbert Krebbers
(Radboud University Nijmegen, Netherlands; Imperial College London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p378-p doi:10.1145/3808303

Verifying Array Properties in Pure Data-Parallel Programs
Nikolaj Hey Hinnerskov, Robert Schenck, and Cosmin Oancea
(University of Copenhagen, Denmark; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p388-p doi:10.1145/3808304

Verification Modulo Tested Library Contracts
Abhishek Uppar, Omar Muhammad, Sumanth Prabhu S, Deepak D'Souza, P. Madhusudan, and Adithya Murali
(IISc Bangalore, India; Relyance AI, India; University of Illinois Urbana-Champaign, USA; University of Wisconsin-Madison, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p396-p doi:10.1145/3808305

Soteria: Efficient Symbolic Execution as a Functional Library: Perhaps You Should Write Your Own Symbolic Execution Engine!
Sacha-Élie Ayoun, Opale Sjöstedt, and Azalea Raad
(Imperial College London, UK; Soteria Tools, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p402-p doi:10.1145/3808306

A Categorical Basis for Robust Program Analysis
Zachary Kincaid and Shaowei Zhu
(Princeton University, USA)

Publisher's Version Article: pldi26main-p410-p doi:10.1145/3808307

SAIL: Sound Abstract Interpreters with LLMs
Qiuhan Gu, Avaljot Singh, and Gagandeep Singh
(University of Illinois Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p429-p doi:10.1145/3808308

Intrinsically Correct Algorithms and Recursive Coalgebras
Cass Alexandru, Henning Urbat, and Thorsten Wißmann
(RPTU Kaiserslautern-Landau, Germany; Radboud University Nijmegen, Netherlands; Friedrich-Alexander University Erlangen-Nürnberg, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p434-p doi:10.1145/3808309

Revisiting Partial Tracing for Safe, Efficient, and Concurrent Garbage Collection in Unmanaged Languages
Jeonghyeon Kim, Jongse Park, Youngjin Kwon, and Jeehoon Kang
(KAIST, Republic of Korea; FuriosaAI, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p438-p doi:10.1145/3808310

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic
Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen, Kwing Hei Li, Joseph Tassarotti, and Lars Birkedal
(Aarhus University, Denmark; New York University, USA; AWS, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p444-p doi:10.1145/3808311

Optimal Predicate Pushdown Synthesis
Robert Zhang, Eric Hayden Campbell, Dixin Tang, and Işıl Dillig
(University of Texas at Austin, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p463-p doi:10.1145/3808312

SparseZETA: Intelligent Auto-tuner for Designing High-Performance SpMV Programs
Zhen Du, Ying Liu, Xionghui Chen, Yanbo Zhao, Xiaobing Feng, Huimin Cui, and Jiajia Li
(Institute of Computing Technology at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Nanjing University, China; North Carolina State University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p473-p doi:10.1145/3808313

Hybrid Path-Sums for Hybrid Quantum Programs
Christophe Chareton, Jad Issa, Mathieu Nguyen, Nicolas Blanco, and Sébastien Bardin
(CEA List - Université Paris-Saclay, France; Université de Lorraine - CNRS - Inria - LORIA, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p478-p doi:10.1145/3808314

Fixed Parameter Tractable Linearizability Monitoring
Zheng Han Lee and Umang Mathur
(National University of Singapore, Singapore)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p482-p doi:10.1145/3808315

Incremental Computation for Efficient Programmable Inference in Probabilistic Programs
Fabian Zaiser, Jack Czenszak, Martin C. Rinard, Vikash K. Mansinghka, and Alexander K. Lew
(Massachusetts Institute of Technology, USA; Yale University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p491-p doi:10.1145/3808316

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, and Chung-Kil Hur
(Seoul National University, Republic of Korea; Yonsei University, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p498-p doi:10.1145/3808317

Weighted NetKAT: A Programming Language for Quantitative Network Verification
Emmanuel Suárez Acevedo, Tiago Ferreira, Kevin Batz, Oliver Bøving, Nate Foster, and Alexandra Silva
(Cornell University, USA; University College London, UK; Technical University of Denmark, Denmark; EPFL, Switzerland; Jane Street, USA)

Publisher's Version Article: pldi26main-p501-p doi:10.1145/3808318

Implementability of Global Distributed Protocols Modulo Network Architectures
Elaine Li and Thomas Wies
(New York University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p510-p doi:10.1145/3808319

Enumerating Ill-Typed Programs for Testing Type Analyzers
Thodoris Sotiropoulos and Zhendong Su
(ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p517-p doi:10.1145/3808320

GradInf: Gradient Estimation as Probabilistic Inference
Gaurav Arya, Mathieu Huot, Moritz Schauer, Alexander K. Lew, and Feras A. Saad
(Carnegie Mellon University, USA; Massachusetts Institute of Technology, USA; Chalmers University of Technology - University of Gothenburg, Sweden; Yale University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p518-p doi:10.1145/3808321

Nested Inductive Types: Justified and Usable Nested Inductive Types in Lean and Rocq
Thomas Lamiaux, Yannick Forster, Matthieu Sozeau, and Nicolas Tabareau
(Nantes Université, France; Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p530-p doi:10.1145/3808322

Typestate via Revocable Capabilities
Songlin Jia, Craig Liu, Siyuan He, Haotian Deng, Yuyan Bao, and Tiark Rompf
(Purdue University, USA; Augusta University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p532-p doi:10.1145/3808323

Persistent Iterators with Value Semantics
Yihe Li and Gregory J. Duck
(National University of Singapore, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p537-p doi:10.1145/3808324

VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type System
Travis Hance, Laila Elbeheiry, Yusuke Matsushita, and Derek Dreyer
(MPI-SWS, Germany; Kyoto University, Japan)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p559-p doi:10.1145/3808325

Restart and Refine: Scalable IFDS Taint Analysis across Memory Budgets
Yujiang Gui, Yonggang Tao, and Jingling Xue
(UNSW, Australia)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p561-p doi:10.1145/3808326

Redundant Array Computation Elimination
Zixuan Wang, Liang Yuan, Xianmeng Jiang, Kun Li, Junmin Xiao, and Yunquan Zhang
(Institute of Computing Technology at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p566-p doi:10.1145/3808327

Hyper Separation Logic
Trayan Gospodinov, Peter Müller, and Thibault Dardinier
(INSAIT at Sofia University St. Kliment Ohridski, Bulgaria; ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p595-p doi:10.1145/3808328

The Search for Constrained Random Generators
Harrison Goldstein, Hila Peleg, Cassia Torczon, Daniel Sainati, Leonidas Lampropoulos, and Benjamin C. Pierce
(SUNY Buffalo, USA; Technion, Israel; University of Pennsylvania, USA; University of Maryland at College Park, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p622-p doi:10.1145/3808329

An Efficient Algorithm for Streaming BPE Tokenization
Konstantinos Mamouras, Angela W. Li, and Yudi Yang
(Rice University, USA)

Publisher's Version Artifacts Functional Article: pldi26main-p647-p doi:10.1145/3808330

Uniformity Analysis in the WebGPU Shading Language
James Lee-Jones, John Wickerson, and Alastair F. Donaldson
(Imperial College London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p659-p doi:10.1145/3808331

Expecto: Extracting Formal Specifications from Natural Language Description for Trustworthy Oracles
Dongjae Lee and Kihong Heo
(KAIST, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p660-p doi:10.1145/3808332

Synthesizing Backward Error Bounds, Backward
Laura Zielinski and Justin Hsu
(Cornell University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p665-p doi:10.1145/3808333

Responsive Parallelism with Dynamic and First-Class Priorities
Marelle León, My Dinh, and Stefan K. Muller
(Illinois Institute of Technology, USA; University of Connecticut, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p701-p doi:10.1145/3808334

Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao, and Tiark Rompf
(Purdue University, USA; Tufts University, USA; Augusta University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p703-p doi:10.1145/3808335

Syntactic Implicit Parameters with Static Overloading
Daan Leijen and Tim Whiting
(Microsoft Research, USA; Brigham Young University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p717-p doi:10.1145/3808336

A Verified Parallel Scheduler for OCaml 5
Clément Allain and Gabriel Scherer
(Inria, France; Université Paris Cité, France)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p742-p doi:10.1145/3808337

Neuro-symbolic Hierarchical Learning for Long-Horizon Robotic Tasks
Yu Huang, Ziji Wu, Zhengyi Ma, Kexin Ma, and Ji Wang
(National University of Defense Technology, China)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p772-p doi:10.1145/3808338

SuperCollider: Scalable and Effective Data Race Detection for CUDA
Mark Stephenson, Sana Damani, Mohamed Tarek Ibn Ziad, Anis Ladram, and Michael Garland
(NVIDIA, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi26main-p774-p doi:10.1145/3808339

Pantomime: Constructive Leakage Proofs via Simulation
Robin Webbers, Robert Schenck, Wind Wong, Kristina Sojakova, and Klaus von Gleissenthall
(Vrije Universiteit Amsterdam, Netherlands; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p785-p doi:10.1145/3808340

Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
Eden Frenkel, Kenneth L. McMillan, Oded Padon, and Sharon Shoham
(Tel Aviv University, Israel; University of Texas at Austin, USA; Weizmann Institute of Science, Israel)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p807-p doi:10.1145/3808341

Scalable Floating-Point Satisfiability via Staged Optimization
Yuanzhuo Zhang, Zhoulai Fu, and Binoy Ravindran
(Virginia Tech, USA; SUNY Korea, Republic of Korea; Stony Brook University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p828-p doi:10.1145/3808342

Categorical Semantics of Probabilistic Symbolic Execution
John M. Li, Jack Czenszak, and Steven Holtzen
(Northeastern University, USA; Yale University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p831-p doi:10.1145/3808343

Navigating AND–OR Graph Modifications to Debug Failing Proof Search
Justin Lubin, Marlena Preigh, Max Willsey, and Sarah E. Chasins
(University of California at Berkeley, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p879-p doi:10.1145/3808344

Compiling to Recurrent Neurons
Joey Velez-Ginorio, Nada Amin, Konrad Kording, and Steve Zdancewic
(University of Pennsylvania, USA; Harvard University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p881-p doi:10.1145/3808345

Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation
Shaurya Gomber, Debangshu Banerjee, and Gagandeep Singh
(University of Illinois Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p887-p doi:10.1145/3808346

TreeCoder: Systematic Exploration and Optimisation of Decoding and Constraints for LLM Code Generation
Henrijs Princis, Arindam Sharma, and Cristina David
(University of Bristol, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p906-p doi:10.1145/3808347

Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification
Satoshi Kura, Hiroshi Unno, and Takeshi Tsukada
(Waseda University, Japan; Tohoku University, Japan; Chiba University, Japan)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p950-p doi:10.1145/3808348

EREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination
Ekaterina Zhuchko, Ian Erik Varatalu, Margus Veanes, and Nikolaj Bjørner
(Tallinn University of Technology, Estonia; Microsoft Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p993-p doi:10.1145/3808349

A Formally Verified Foundation for Compositional Heterogeneous Coherence
An Qi Zhang, Andrés Goens, Daniel Sorin, and Vijay Nagarajan
(University of Utah, USA; TU Darmstadt, Germany; Duke University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p1012-p doi:10.1145/3808350

Abstract Interpretation with Confidence: Quantifying the Precision of Dataflow Analysis with Probabilities
Yuanfeng Shi, Ziyue Jin, and Xin Zhang
(Peking University, China)

Publisher's Version Article: pldi26main-p1066-p doi:10.1145/3808351

Dynamically Checked Deep Immutability in Python
Fridtjof Stoldt, Sylvan Clebsch, Matthew A. Johnson, Matthew J. Parkinson, and Tobias Wrigstad
(Uppsala University, Sweden; Microsoft Azure Research, USA; Microsoft Azure Research, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p1129-p doi:10.1145/3808352

Corrigendum: Falcon: A Scalable Analytical Cache Model
Arjun Pitchanathan, Kunwar Grover, and Tobias Grosser
(University of Edinburgh, UK; Advanced Micro Devices, UK; University of Cambridge, UK)

Publisher's Version Article: pldi24main-p644-p-CR doi:10.1145/3820287