PLDI 2026 Research Papers — Wed 17 Jun
Table of Contents
- Cross-connections to our notes
- Keynote (09:00, Flatirons 2+3+4)
- Sessions (relevant subset)
- Abstract Interpretation (16:10, chair: Mukund Raghothaman, USC)
- GPU Programming (16:10, chair: Gilbert Louis Bernstein, UW)
- Type Systems (16:10, chair: Eleftherios Ioannidis, MSR)
- Mechanized Program Logics & Verification (11:00, chair: Yusuke Matsushita, Kyoto)
- Specification Synthesis & Verification (11:00, chair: John Regehr, Utah)
- Networking & Distributed Systems (14:00, chair: Mae Milano, Princeton)
- References
Selected from the Wed 17 Jun program (PLDI 2026). The bib holds the papers that touch our threads; this note maps them to the threads and the recurring speakers.
Cross-connections to our notes
| Paper | Thread / note | Speaker also in |
|---|---|---|
| SAIL: Sound Abstract Interpreters with LLMs (Gu, Singh, and Singh 2026) | abstract interp + LLMs | Gagandeep Singh — PAgE keynote (formal methods for frontier AI) |
| Evolving Abstract Transformers (Gomber, Banerjee, and Singh 2026) | abstract interp | Singh group |
| Kuiper (Mart\’ınez et al. 2026), SIMT-Step (Chen et al. 2026) | dependent types + GPU verification | Martínez, Sorensen — PAgE "AI-generated kernels" |
| Modular GPU / Typed Perspectives (Bansal et al. 2026) (Distinguished) | type systems | Amarasinghe, Ragan-Kelley (Wed keynote) |
| Probabilistic Refinement Session Types (Fu, Das, and Gaboardi 2026) | type systems + choreography | Ankush Das — CP 2026 consensus-choreography work |
| Implementability of Global Distributed Protocols (Li and Wies 2026) | choreographies / EPP | the CP 2026 core question |
| Reachability Types (Deng et al. 2026), Typestate via Capabilities (Jia et al. 2026) | the affine/ownership cell of One Tool, Four Ways | Rompf group |
| A Deductive System for Contract Satisfaction (Correnson, Zeng, and Hofmann 2026) | contracts/blame (Findler-Blume, YDF) | — |
| Code-Specify-Test-Debug-Prove (Aamer et al. 2026) | spec workflows / verify-first | Benjamin C. Pierce (cf. pierce2002tapl), Sewell |
| Counterexample-Guided Inference of Modular Specs (Hallahan, Jhala, and Piskac 2026) | spec inference | Ranjit Jhala (cf. jhala2021refinement) |
| Expecto: specs from natural language (Lee and Heo 2026) | the spec-validation frontier | — |
| LLMEffect: typing LLM API boundaries (Sen 2026) (SRC) | agentic / spect8r BYO-endpoint | — |
The through-line: PLDI 2026's main track is heavy on LLMs producing verified artifacts (SAIL, Expecto, LLMEffect) and the type disciplines our four-ways note catalogs (reachability, typestate, refinement-session, dependent+separation), with the same handful of people (Singh, Sorensen/Martínez, Das, Pierce, Jhala, Rompf) spanning PAgE, CP, and the main track.
Keynote (09:00, Flatirons 2+3+4)
Programming Language Design and Implementation for the Machine Learning Era: A Personal Perspective — Saman Amarasinghe (MIT). Chair: Manu Sridharan (UC Riverside).
Sessions (relevant subset)
Abstract Interpretation (16:10, chair: Mukund Raghothaman, USC)
- SAIL: Sound Abstract Interpreters with LLMs — Gu, A. Singh, G. Singh (UIUC) (Gu, Singh, and Singh 2026)
- Evolving Abstract Transformers for Gradient-Guided Abstract Interpretation — Gomber, Banerjee, G. Singh (UIUC) (Gomber, Banerjee, and Singh 2026)
- Abstract Interpretation with Confidence — Shi, Jin, X. Zhang (Peking)
- Optimism in Equality Saturation — Arbore, Cheung, Willsey (UC Berkeley)
GPU Programming (16:10, chair: Gilbert Louis Bernstein, UW)
- Kuiper: Correct & Efficient GPU Programming with Dependent Types + Separation Logic — Martínez, Köpcke, Fiala, Ebner, Ramananandro, Steuwer, Sorensen, Swamy (MSR/TUB/ETH) (Mart\’ınez et al. 2026)
- Modular GPU Programming with Typed Perspectives (Distinguished) — Bansal, Sainati, Cutler, Amarasinghe, Ragan-Kelley (MIT/Penn) (Bansal et al. 2026)
- StreamAlloc [TOPLAS] — Basu, Vedurada (IIT Hyderabad)
- SIMT-Step Execution: Operational Semantics for GPU Subgroups — Chen, Rehman, Martínez, Sorensen (UCSC/UCSB/MSR) (Chen et al. 2026)
- Uniformity Analysis in the WebGPU Shading Language — Lee-Jones, Wickerson, Donaldson (Imperial)
Type Systems (16:10, chair: Eleftherios Ioannidis, MSR)
- Probabilistic Refinement Session Types — Fu, Das, Gaboardi (BU) (Fu, Das, and Gaboardi 2026)
- Complete the Cycle: Reachability Types with Cyclic References — Deng, He, Jia, Bao, Rompf (Purdue/Augusta) (Deng et al. 2026)
- Backwards-Compatible Row-Based Exceptions in ML — van Collem, de Vilhena, Krebbers (Radboud/Imperial) (van Collem, de Vilhena, and Krebbers 2026)
- Typestate via Revocable Capabilities — Jia, Liu, He, Deng, Bao, Rompf (Purdue/Augusta) (Jia et al. 2026)
- Syntactic Implicit Parameters with Static Overloading — Leijen (MSR), Whiting (BYU) (Leijen and Whiting 2026)
Mechanized Program Logics & Verification (11:00, chair: Yusuke Matsushita, Kyoto)
- A Deductive System for Contract Satisfaction Proofs — Correnson, Zeng, Hofmann (CISPA/Harvard/MPI-SP) (Correnson, Zeng, and Hofmann 2026)
- A Mechanized Algebra of Verified Data Structures for Sparse Tensor Programs — Liu, Bernstein, Kamil, Chlipala, Ragan-Kelley (MIT/UW/Adobe)
- Iris-WasmFX: Modular Reasoning for Wasm Stack Switching — Legoupil, Pedersen, Birkedal, Lindley, Pichon-Pharabod
- Code-Specify-Test-Debug-Prove — Aamer, …, Pierce, Pulte, Sewell (Penn/Cambridge/Oxford) (Aamer et al. 2026)
- Cerisier: Program Logic for Attestation in a Capability Machine — Rousseau, Carnier, Van Strydonck, Keuchel, Devriese, Birkedal
Specification Synthesis & Verification (11:00, chair: John Regehr, Utah)
- Counterexample-Guided Inference of Modular Specifications — Hallahan, Jhala, Piskac (Hallahan, Jhala, and Piskac 2026)
- Verification Modulo Tested Library Contracts — Uppar, Muhammad, Prabhu, D'Souza, Madhusudan, Murali (Uppar et al. 2026)
- Expecto: Extracting Formal Specifications from Natural Language — Lee, Heo (KAIST) (Lee and Heo 2026)
- (also: Choose Don't Label, Presynthesis)
Networking & Distributed Systems (14:00, chair: Mae Milano, Princeton)
- Implementability of Global Distributed Protocols Modulo Network Architectures — Li, Wies (NYU) (Li and Wies 2026)
- SureDistrib: Almost-Sure Termination of Byzantine Protocols — Qiu, Xiao, Shin, Shao (Yale/HKU/Northeastern) (Qiu et al. 2026)
- MatchBox (Distinguished), Weighted NetKAT (Foster, Silva), Heterogeneous Coherence
Other Wed sessions (not bib'd here): Quantum Computing (Ying/Zhang Distinguished; Yuan Distinguished), Concurrency (DPOR, linearizability, CUDA races), Static Analysis 1. SRC posters of note: LLMEffect (Sen 2026).
References
Aamer, Zain K., Rini Banerjee, Hiroyuki Katsura, David Kaloper-Meršinjak, Dimitrios J. Economou, Kayvan Memarian, Dhruv Makwana, et al. 2026. “Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows.” In Proc. Acm Pldi. https://doi.org/10.1145/3808278.
Bansal, Manya, Daniel Sainati, Joseph W. Cutler, Saman Amarasinghe, and Jonathan Ragan-Kelley. 2026. “Modular Gpu Programming with Typed Perspectives.” In Proc. Acm Pldi. https://doi.org/10.1145/3808290.
Chen, Zheyuan, Naomi Rehman, Guido Mart\’ınez, and Tyler Sorensen. 2026. “Simt-Step Execution: A Flexible Operational Semantics for Gpu Subgroup Behavior.” In Proc. Acm Pldi. https://doi.org/10.1145/3808297.
Collem, Simcha van, Paulo Em\’ılio de Vilhena, and Robbert Krebbers. 2026. “Backwards-Compatible Row-Based Exceptions in Ml.” In Proc. Acm Pldi. https://doi.org/10.1145/3808303.
Correnson, Arthur, Haoyi Zeng, and Jana Hofmann. 2026. “A Deductive System for Contract Satisfaction Proofs.” In Proc. Acm Pldi. https://doi.org/10.1145/3808251.
Deng, Haotian, Siyuan He, Songlin Jia, Yuyan Bao, and Tiark Rompf. 2026. “Complete the Cycle: Reachability Types with Expressive Cyclic References.” In Proc. Acm Pldi.
Fu, Qiancheng, Ankush Das, and Marco Gaboardi. 2026. “Probabilistic Refinement Session Types.” In Proc. Acm Pldi.
Gomber, Shaurya, Debangshu Banerjee, and Gagandeep Singh. 2026. “Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation.” In Proc. Acm Pldi. https://doi.org/10.1145/3808346.
Gu, Qiuhan, Avaljot Singh, and Gagandeep Singh. 2026. “Sail: Sound Abstract Interpreters with Llms.” In Proc. Acm Pldi. https://doi.org/10.1145/3808308.
Hallahan, William, Ranjit Jhala, and Ruzica Piskac. 2026. “Counterexample-Guided Inference of Modular Specifications.” In Proc. Acm Pldi.
Jia, Songlin, Craig Liu, Siyuan He, Haotian Deng, Yuyan Bao, and Tiark Rompf. 2026. “Typestate via Revocable Capabilities.” In Proc. Acm Pldi. https://doi.org/10.1145/3808323.
Lee, Dongjae, and Kihong Heo. 2026. “Expecto: Extracting Formal Specifications from Natural Language Description for Trustworthy Oracles.” In Proc. Acm Pldi. https://doi.org/10.1145/3808332.
Leijen, Daan, and Tim Whiting. 2026. “Syntactic Implicit Parameters with Static Overloading.” In Proc. Acm Pldi. https://doi.org/10.1145/3808336.
Li, Elaine, and Thomas Wies. 2026. “Implementability of Global Distributed Protocols modulo Network Architectures.” In Proc. Acm Pldi. https://doi.org/10.1145/3808319.
Mart\’ınez, Guido, Bastian Köpcke, Jonáš Fiala, Gabriel Ebner, Tahina Ramananandro, Michel Steuwer, Tyler Sorensen, and Nikhil Swamy. 2026. “Kuiper: Correct and Efficient Gpu Programming with Dependent Types and Separation Logic.” In Proc. Acm Pldi. https://doi.org/10.1145/3808280.
Qiu, Longfei, Jingqi Xiao, Ji-Yong Shin, and Zhong Shao. 2026. “Suredistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine Protocols.” In Proc. Acm Pldi. https://doi.org/10.1145/3808293.
Sen, Sanjib Kumar. 2026. “Llmeffect: A Type System for Securing Llm Api Boundaries.” PLDI 2026 Student Research Competition.
Uppar, Abhishek, Omar Muhammad, Sumanth Prabhu S, Deepak D’Souza, P. Madhusudan, and Adithya Murali. 2026. “Verification modulo Tested Library Contracts.” In Proc. Acm Pldi. https://doi.org/10.1145/3808305.