Six papers accepted at PLDI 2026

The conference takes place in Boulder, Colorado, USA, in June 2026 and brings together leading researchers from around the world working on programming languages, verification, software security, compilers, and systems. 

The six accepted papers span topics including formal verification, privacy-preserving computation, trusted computing, WebAssembly, concurrency analysis, and memory safety. 

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs 
Authors: Kwing Hei Li (Aarhus University), Alejandro Aguirre (Aarhus University), Joseph Tassarotti (New York University), Lars Birkedal (Aarhus University) 
https://iris-project.org/pdfs/2026-pldi-foxtrot.pdf 
The paper introduces Foxtrot, the first higher-order separation logic for proving correctness properties of concurrent probabilistic programs, enabling rigorous reasoning about systems that combine randomness and concurrency. 

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic 
Authors: Philipp G. Haselwarter (Aarhus University), Alejandro Aguirre (Aarhus University), Simon Oddershede Gregersen (CISPA Helmholtz Center for Information Security), Kwing Hei Li (Aarhus University), Joseph Tassarotti (New York University), Lars Birkedal (Aarhus University)
https://pure.au.dk/portal/en/publications/modular-verification-of-differential-privacy-in-probabilistic-hig/ 
The researchers present a new program logic for verifying implementations of differentially private algorithms in realistic programming languages, supporting modular reasoning about privacy-preserving software libraries. 

Cerisier: A Program Logic for Attestation in a Capability Machine
Authors: June Rousseau (Aarhus University), Denis Carnier (KU Leuven), Thomas Van Strydonck (Fortanix), Steven Keuchel (KU Leuven), Dominique Devriese (KU Leuven), Lars Birkedal (Aarhus University) 
https://arxiv.org/pdf/2604.13638 
This work introduces the first program logic for modular reasoning about attestation in trusted computing systems, enabling formal verification of software that combines trusted, untrusted, and attested code.  

Iris-WasmFX: Modular Reasoning for Wasm Stack Switching 
Authors: Maxime Legoupil (Nanyang Technological University), Mathias Pedersen (Aarhus University), Lars Birkedal (Aarhus University), Sam Lindley (University of Edinburgh), Jean Pichon-Pharabod (Aarhus University) 
https://homepages.inf.ed.ac.uk/slindley/papers/iris-wasmfx-draft-november2025.pdf 
The paper develops formal foundations and verification techniques for WasmFX, a proposed WebAssembly extension that supports advanced control-flow mechanisms such as effect handlers, coroutines, and generators. 

Fast Atomicity Monitoring 
Authors: Hünkar Can Tunç (Uber), Yifan Dong (Aarhus University), Andreas Pavlogiannis (Aarhus University) 
https://arxiv.org/pdf/2604.11369 
The researchers present AtomSanitizer, a new algorithm for detecting atomicity violations in concurrent software. The approach is both theoretically faster and practically more efficient than previous methods and can be used for real-time monitoring. 

The Downgrading Semantics of Memory Safety 
Authors: René Rydhof Hansen (Aalborg University), Andreas Stenbæk Larsen (Aarhus University), Aslan Askarov (Aarhus University) 
https://arxiv.org/pdf/2507.11282 
This paper proposes a new semantic foundation for memory safety, providing a principled framework for understanding memory errors such as use-after-free, double-free, and heap overflows. 

About PLDI 

PLDI (Programming Language Design and Implementation) is ACM SIGPLAN's flagship conference on programming languages and programming systems research. It is widely regarded as one of the most prestigious venues in the field, bringing together researchers working on programming language design, implementation, verification, software security, compilers, and systems. Find more information about the conference here: https://pldi26.sigplan.org/