PLDI 2026
Basics
| Field | Value |
|---|---|
| Dates | – |
| Venue | Limelight Boulder, Boulder, Colorado |
| Host | ACM SIGPLAN |
| URL | pldi26.sigplan.org |
| Format | Multi-track with co-located events, workshops, tutorials |
| Framing | PL research, compilers, verification; PAgE workshop on agentic engineering |
Co-located conferences
- ISMM 2026 — International Symposium on Memory Management
- LCTES 2026 — Languages, Compilers, and Tools for Embedded Systems
Workshops
| Workshop | Full name | Notes |
|---|---|---|
| ARRAY 2026 | Array-oriented Programming | |
| CP 2026 | Choreographic Programming | |
| EGRAPHS | Equality Graphs | E-graph rewriting, optimization |
| PAgE 2026 | Principles of Agentic Engineering | Formal foundations for agent safety/reliability |
| PLMW | PL Mentoring Workshop | |
| PROPL | Programming for the Planet | |
| SOAP 2026 | State of the Art in Program Analysis | |
| — | Tom Ball at Sixty | Celebration session |
Tutorials
- Writing Performance-Portable Kernels Simplified with Helion
- A guided tour through Oxidized OCaml
- Implementing an Integrated Development Environment
- Mechanized Specifications for Real-World Programming Languages
- ACT: End-to-End Compiler Infrastructure for Emerging AI Accelerators
- Deep dive into the AWS Nitro Isolation Engine
PAgE 2026 — Principles of Agentic Engineering
The workshop most directly connected to current research.
| Field | Value |
|---|---|
| Date | |
| Deadline | 2026-05-06 AoE |
| Portal | page2026.hotcrp.com |
| Contact | sbarke@microsoft.com |
Organizing committee
- Shraddha Barke (Microsoft Research, Redmond)
- Peli de Halleux (Microsoft Research)
- Dan Grossman (University of Washington)
- Madan Musuvathi (Microsoft Research)
- Dawn Song (UC Berkeley)
- Ben Zorn (Microsoft)
Submission tracks
- Archived papers (up to 10 pages) — published in ACM Digital Library
- Non-archival submissions (up to 6 pages) — work in progress, position papers, demos
Why PAgE matters
"AI-powered agents increasingly deployed in production settings require formal foundations for safety and reliability through agentic engineering principles."
This is the PL community's formal-methods entry point into agent governance — the same territory BugBash approaches from the testing/DST side and ELS approaches from the Lisp/MOP side. The committee (Grossman, Song, Zorn) carries enough weight to set vocabulary that sticks.
Program (Mon 15 Jun 2026, Meadows CD)
Tentative; chaired by Shraddha Barke. Two keynotes bracket two sessions.
| Time | Talk | Who |
|---|---|---|
| 09:10 | Keynote: Formal Methods for Frontier AI Systems | Gagandeep Singh (UIUC) |
| 10:40 | Agentic Code Reasoning | Ugare, Chandra (Meta) |
| 11:00 | Towards Verified Code Reasoning by LLMs | Sistla et al. (Google DeepMind) |
| 11:20 | Testing LLM-Generated Distributed Protocol Code | Das, Coyne (Boston U.) |
| 11:40 | The Next Frontier for AI-Generated Kernels: Correctness | Martínez (MSR), Sorensen (UCSC) |
| 12:00 | Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code | Rinard (MIT) |
| 13:40 | Combining Agentic AI and Lightweight Formal Methods to Find Bugs in a Production Hypervisor | Katsura, Memarian, Sewell (Cambridge) |
| 14:00 | From Workarounds to Root Causes: Agentic Workflows on Browser GPU Compiler Stacks | Ramesh, Levine, Sorensen (UCSC) |
| 14:20 | Event-based Design Abstractions for Agent Harnesses | Becker, Ghavami, … Rinard, Mansinghka (MIT) |
| 14:40 | Lumos: Let there be Language Model System Certification | Chaudhary et al. (UIUC) |
| 15:00 | Lazy Validation and Self-Healing for Agentic Programs | Tsampouris, Ioannidis (MSR), Symeonidis |
| 15:50 | Keynote: Can Coding Agents Write Verifiably Correct Software? | Shan Lu (Microsoft / UChicago) |
Closest to the reversible-pipeline verification thread: Rinard's Axon
verified compiler in Lean and Claude Code and the Cambridge lightweight formal
methods + agentic AI hypervisor work — both the verification-first,
agent-drives-the-prover pattern we used for the Lean Equiv and Dafny codec
proofs. Shan Lu's closing keynote — can coding agents write verifiably correct
software? — is the experiment those proofs run.
Why
PLDI sits at the intersection of formal methods and practical compiler engineering. Three reasons this year matters:
- PAgE workshop. First SIGPLAN-affiliated venue explicitly framed as "agentic engineering." The formal-methods community claiming this term has downstream consequences for how agent governance gets specified. The elenctic-spec framing and Seven Concerns layering should be testable against whatever vocabulary PAgE settles on.
- Nitro Isolation Engine tutorial. AWS Nitro is the production hypervisor-isolation analog to Antithesis. The tutorial is a data point on how far hardware-backed isolation has moved since BugBash.
- Egraphs workshop. E-graph rewriting is the optimization substrate beneath equality saturation. Relevant to any spec-refinement system that needs to normalize equivalent representations — the same problem elenctic-spec faces at the methodology layer.
Refutation
The PAgE framing for this event is wrong if:
- The workshop is dominated by LLM-agent benchmarking rather than formal foundations (safety/reliability becomes eval leaderboards).
- The "agentic engineering" vocabulary diverges completely from the Seven Concerns framing, with no productive mapping between them.
- The Nitro tutorial is marketing rather than technical substrate.
In those cases PLDI reduces to a compiler conference with an adjacent agent workshop that didn't converge on useful primitives.
Concern mapping
| Event/Talk | Concern | Claim under test |
|---|---|---|
| PAgE workshop (overall) | L3, L7 | PL community can formalize agent governance primitives |
| Grossman/Song/Zorn committee | L3 | Formal methods vocabulary for agents will be PL-native |
| Nitro Isolation Engine | L1, L5 | Hardware isolation composes with agent sandboxing |
| Egraphs workshop | L2, L3 | Equality saturation applies to spec normalization |
| Mechanized Specifications | L3 | Mechanized specs are the reader-as-spec-emitter generalized |
| Oxidized OCaml tutorial | L1, L2 | Rust ownership model transfers to ML family |
Related
- BugBash 2026 — Antithesis, DST, software correctness; the testing-side complement to PAgE's formal-methods framing
- ELS 2026 — European Lisp Symposium; MOP and reader-as-protocol are the Lisp-side complement
- TLA+ System Design — formal specification practice, directly relevant to PAgE submissions
- Agentic Systems 2026 — Seven Concerns framework that PAgE vocabulary should map to
- Elenctic Vibe Code Review — the review discipline PAgE might formalize
- Lean4 on FreeBSD — theorem proving toolchain, mechanized specification substrate
- Agent Isolation with FreeBSD Jails — local isolation counterpart to Nitro tutorial