PLDI 2026 - PLDI Research Papers

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT-06:00) Mountain Time (US & Canada).

Use conference time zone: (GMT-06:00) Mountain Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

You're viewing the program in a time zone which is different from your device's time zone change time zone

Wed 17 Jun
Displayed time zone: Mountain Time (US & Canada) change

09:00 - 10:10	Keynote 1PLDI Research Papers at Flatirons 2-3-4

09:00 70m Keynote		Programming Language Design and Implementation for the Machine Learning Era: A Personal Perspective PLDI Research Papers Saman Amarasinghe Massachusetts Institute of Technology

10:30 - 12:10	Mechanized Program Logics and VerificationPLDI Research Papers at Flatirons 2

10:30 20m Talk		A Deductive System for Contract Satisfaction Proofs PLDI Research Papers Arthur Correnson CISPA Helmholtz Center for Information Security, Haoyi Zeng Harvard University, Jana Hofmann MPI-SP DOI Pre-print
10:50 20m Talk		A Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs PLDI Research Papers Amanda Liu Massachusetts Institute of Technology, Gilbert Louis Bernstein University of Washington, Shoaib Kamil Adobe, Adam Chlipala Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology DOI
11:10 20m Talk		Iris-WasmFX: Modular Reasoning for Wasm Stack Switching PLDI Research Papers Maxime Legoupil Nanyang Technological University, Mathias Pedersen Aarhus University, Lars Birkedal Aarhus University, Sam Lindley University of Edinburgh, Jean Pichon-Pharabod Aarhus University DOI
11:30 20m Talk		Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows PLDI Research Papers Zain K Aamer University of Pennsylvania, Rini Banerjee University of Cambridge, Hiroyuki Katsura University of Cambridge, David Kaloper-Meršinjak University of Cambridge, Dimitrios J. Economou University of Cambridge, Kayvan Memarian University of Cambridge, Dhruv Makwana University of Cambridge, Neel Krishnaswami University of Cambridge, Benjamin C. Pierce University of Pennsylvania, Christopher Pulte University of Oxford, Peter Sewell University of Cambridge DOI Pre-print
11:50 20m Talk		Cerisier: A Program Logic for Attestation in a Capability Machine PLDI Research Papers June Rousseau Aarhus University, Denis Carnier KU Leuven, Thomas Van Strydonck Fortanix, Steven Keuchel KU Leuven, Dominique Devriese KU Leuven, Lars Birkedal Aarhus University DOI

10:30 - 12:10	Specification Synthesis and VerificationPLDI Research Papers at Flatirons 3

10:30 20m Talk		[SIGPLAN] Counterexample-Guided Inference of Modular Specifications PLDI Research Papers William Hallahan Binghamton, Ranjit Jhala University of California at San Diego, Ruzica Piskac Yale University
10:50 20m Talk		Choose, Don’t Label: Multiple-Choice Query Synthesis for Program Disambiguation PLDI Research Papers Celeste Barnaby University of Texas at Austin, Danny Ding University of Texas at Austin, Osbert Bastani University of Pennsylvania, Işıl Dillig University of Texas at Austin DOI
11:10 20m Talk		Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics PLDI Research Papers Rui Dong University of Michigan, Qingyue Wu University of Michigan, Danny Ding University of Texas at Austin, Zheng Guo University of Michigan, Ruyi Ji University of Michigan, Xinyu Wang University of Michigan DOI
11:30 20m Talk		Verification Modulo Tested Library Contracts PLDI Research Papers Abhishek Uppar IISc Bangalore, Omar Muhammad IISc Bangalore, Sumanth Prabhu S Relyance AI, Deepak D'Souza IISc Bangalore, P. Madhusudan University of Illinois Urbana-Champaign, Adithya Murali University of Wisconsin-Madison DOI
11:50 20m Talk		Expecto: Extracting Formal Specifications from Natural Language Description for Trustworthy Oracles PLDI Research Papers Dongjae Lee KAIST, Kihong Heo KAIST DOI

10:30 - 12:10	Quantum ComputingPLDI Research Papers at Flatirons 4

10:30 20m Talk		Verification of Recursively Defined Quantum Circuits PLDI Research Papers Mingsheng Ying University of Technology Sydney, Zhicheng Zhang University of Technology Sydney DOI
10:50 20m Talk		SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits PLDI Research Papers Nengkun Yu Stony Brook University, Jens Palsberg University of California at Los Angeles, Thomas Reps University of Wisconsin-Madison DOI
11:10 20m Talk		Hybrid Path-Sums for Hybrid Quantum Programs PLDI Research Papers Christopĥe Chareton CEA List - Université Paris-Saclay, Sébastien Bardin CEA List - Université Paris-Saclay, Jad Issa CEA List - Université Paris-Saclay, Mathieu Nguyen CEA List - Université Paris-Saclay, Nicolas Blanco CEA List - Université Paris-Saclay DOI
11:30 20m Talk		[TOPLAS] VyZX: Formal Verification of a Graphical Quantum Language PLDI Research Papers Adrian Lehmann University of Chicago, Ben Caldwell University of Chicago, A: Bhakti Shah , William Spencer , Robert Rand University of Chicago
11:50 20m Talk		Cobble: Compiling Block Encodings for Quantum Computational Linear Algebra PLDI Research Papers Charles Yuan University of Wisconsin-Madison DOI

13:40 - 15:20	Networking and Distributed SystemsPLDI Research Papers at Flatirons 2

13:40 20m Talk		A Formally Verified Foundation for Compositional Heterogeneous Coherence PLDI Research Papers An Qi Zhang University of Utah, Andrés Goens TU Darmstadt, Daniel Sorin Duke University, Vijay Nagarajan University of Utah DOI
14:00 20m Talk		MatchBox: A Semantic Foundation for Data Plane Portability PLDI Research Papers Eric Hayden Campbell University of Texas at Austin, Robert Zhang University of Texas at Austin, Divyanshu Saxena University of Texas at Austin, Aditya Akella University of Texas at Austin, Işıl Dillig University of Texas at Austin DOI
14:20 20m Talk		SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine Protocols PLDI Research Papers Longfei Qiu Yale University, Jingqi Xiao University of Hong Kong, Ji-Yong Shin Northeastern University, Zhong Shao Yale University DOI
14:40 20m Talk		Implementability of Global Distributed Protocols Modulo Network Architectures PLDI Research Papers Elaine Li New York University, Thomas Wies New York University DOI
15:00 20m Talk		Weighted NetKAT: A Programming Language For Quantitative Network Verification PLDI Research Papers Emmanuel Suárez Acevedo Cornell University, Tiago Ferreira University College London, Kevin Batz Cornell University, Oliver Emil Bøving Technical University of Denmark, Nate Foster EPFL; Jane Street, Alexandra Silva Cornell University DOI

13:40 - 15:20	ConcurrencyPLDI Research Papers at Flatirons 3

13:40 20m Talk		State Space Estimation for DPOR-Based Model Checkers PLDI Research Papers A. R. Balasubramanian MPI-SWS, Mohammad Hossein Khoshechin Jorshari MPI-SWS, Rupak Majumdar MPI-SWS, Umang Mathur National University of Singapore, Minjian Zhang University of Illinois Urbana-Champaign DOI Pre-print
14:00 20m Talk		Fixed Parameter Tractable Linearizability Monitoring PLDI Research Papers Zheng Han Lee National University of Singapore, Umang Mathur National University of Singapore DOI Pre-print
14:20 20m Talk		SuperCollider: Scalable and Effective Data Race Detection for CUDA PLDI Research Papers Mark Stephenson NVIDIA, Sana Damani NVIDIA, Mohamed Tarek Ibn Ziad NVIDIA, Anis Ladram NVIDIA, Michael Garland NVIDIA DOI
14:40 20m Talk		Fast Atomicity Monitoring PLDI Research Papers Hünkar Can Tunç Uber, Yifan Dong Aarhus University, Andreas Pavlogiannis Aarhus University DOI

13:40 - 15:20	Static Analysis 1PLDI Research Papers at Flatirons 4

13:40 20m Talk		Flow-Analysis-Based Closure Optimization PLDI Research Papers John Reppy University of Chicago, Olin Shivers Northeastern University, Byron Zhong University of Chicago DOI
14:00 20m Talk		SSA without Dominance for Higher-Order Programs PLDI Research Papers Roland Leißa University of Göttingen, Johannes Griebler University of Göttingen DOI Pre-print
14:20 20m Talk		Analyzing Bytes: Pre-Disassembly Static Binary Analysis PLDI Research Papers Huan Nguyen Google, Soumyakant Priyadarshan Stony Brook University, Chencheng Jiang Stony Brook University, R. Sekar Stony Brook University DOI
14:40 20m Talk		Exploiting Sophisticated Static Analysis for Verilog PLDI Research Papers Qinlin Chen Nanjing University, Nairen Zhang Nanjing University, Jinpeng Wang Nanjing University, Jiacai Cui Nanjing University, Tian Tan Nanjing University, Xiaoxing Ma Nanjing University, Chang Xu Nanjing University, Jian Lu Nanjing University, Yue Li Nanjing University DOI
15:00 20m Talk		Bridging Coverage and Confidence: Reliable Static False Alarm Elimination via Input-Agnosticity PLDI Research Papers Jiayi Wang Nanjing University, Yu Wang Nanjing University, Linzhang Wang Nanjing University, Ke Wang Nanjing University DOI

15:50 - 17:30	Abstract InterpretationPLDI Research Papers at Flatirons 2

15:50 20m Talk		Path-Sensitive Abstract Interpretation for WCET Estimation PLDI Research Papers Shangshang Xiao Shandong University, Mengxia Sun Shandong University, Wei Zhang Shandong University, Naijun Zhan Peking University; Zhongguancun Laboratory, Lei Ju Shandong University DOI
16:10 20m Talk		SAIL: Sound Abstract Interpreters with LLMs PLDI Research Papers Qiuhan Gu University of Illinois Urbana-Champaign, Avaljot Singh University of Illinois Urbana-Champaign, Gagandeep Singh University of Illinois Urbana-Champaign DOI
16:30 20m Talk		Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation PLDI Research Papers Shaurya Gomber University of Illinois Urbana-Champaign, Debangshu Banerjee University of Illinois Urbana-Champaign, Gagandeep Singh University of Illinois Urbana-Champaign DOI Pre-print
16:50 20m Talk		Abstract Interpretation with Confidence PLDI Research Papers Yuanfeng Shi Peking University, Ziyue Jin Peking University, Xin Zhang Peking University DOI
17:10 20m Talk		Optimism in Equality Saturation PLDI Research Papers Russel Arbore University of California at Berkeley, Alvin Cheung University of California at Berkeley, Max Willsey University of California at Berkeley DOI Pre-print

15:50 - 17:30	GPU ProgrammingPLDI Research Papers at Flatirons 3

15:50 20m Talk		Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic PLDI Research Papers Guido Martínez Microsoft Research, Bastian Köpcke TU Berlin, Jonáš Fiala ETH Zurich, Gabriel Ebner Microsoft Research, Tahina Ramananandro Microsoft Research, Michel Steuwer TU Berlin, Tyler Sorensen Microsoft Research, Nikhil Swamy Microsoft Research DOI
16:10 20m Talk		Modular GPU Programming with Typed Perspectives PLDI Research Papers Manya Bansal Massachusetts Institute of Technology, Daniel Sainati University of Pennsylvania, Joseph W. Cutler University of Pennsylvania, Saman Amarasinghe Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology DOI
16:30 20m Talk		[TOPLAS] StreamAlloc: A Framework for Analyzing and Transforming CUDA Code to Enable Asynchronous Execution PLDI Research Papers Soumik Kumar Basu IIT Hyderabad, Jyothi Vedurada IIT Hyderabad
16:50 20m Talk		SIMT-Step Execution: A Flexible Operational Semantics For GPU Subgroup Behavior PLDI Research Papers Zheyuan Chen University of California at Santa Cruz, Naomi Rehman University of California at Santa Barbara, Guido Martínez Microsoft Research, Tyler Sorensen Microsoft Research; University of California at Santa Cruz DOI
17:10 20m Talk		Uniformity Analysis in the WebGPU Shading Language PLDI Research Papers James Lee-Jones Imperial College London, John Wickerson Imperial College London, Alastair F. Donaldson Imperial College London DOI

15:50 - 17:30	Type SystemsPLDI Research Papers at Flatirons 4

15:50 20m Talk		[SIGPLAN] Probabilistic Refinement Session Types PLDI Research Papers Qiancheng Fu Boston University, Ankush Das Boston University, Marco Gaboardi Boston University
16:10 20m Talk		[SIGPLAN] Complete the Cycle: Reachability Types with Expressive Cyclic References PLDI Research Papers Haotian Deng Purdue University, Siyuan He Purdue University, Songlin Jia Purdue University, Yuyan Bao Augusta University, Tiark Rompf Purdue University
16:30 20m Talk		Backwards-Compatible Row-Based Exceptions in ML PLDI Research Papers Simcha van Collem Radboud University Nijmegen, Paulo Emílio de Vilhena Imperial College London, Robbert Krebbers Radboud University Nijmegen DOI
16:50 20m Talk		Typestate via Revocable Capabilities PLDI Research Papers Songlin Jia Purdue University, Craig Liu Purdue University, Siyuan He Purdue University, Haotian Deng Purdue University, Yuyan Bao Augusta University, Tiark Rompf Purdue University DOI
17:10 20m Talk		Syntactic Implicit Parameters with Static Overloading PLDI Research Papers Daan Leijen Microsoft Research, Tim Whiting Brigham Young University DOI Pre-print

Thu 18 Jun
Displayed time zone: Mountain Time (US & Canada) change

09:00 - 10:10	Keynote 2PLDI Research Papers at Flatirons 2-3-4

09:00 70m Keynote		Happiness U-Curve: Navigating the AI Validation Bottleneck PLDI Research Papers Miryung Kim UCLA and Amazon Web Services

10:30 - 11:50	Symbolic Methods for Verification and MatchingPLDI Research Papers at Flatirons 2

10:30 20m Talk		Solvable Tuple Patterns and Their Applications to Program Verification PLDI Research Papers Naoki Kobayashi University of Tokyo, Ryosuke Sato Tokyo University of Agriculture and Technology, Ayumi Shinohara Tohoku University, Ryo Yoshinaka Tohoku University DOI
10:50 20m Talk		An Efficient Algorithm for Streaming BPE Tokenization PLDI Research Papers Konstantinos Mamouras Rice University, Angela W. Li Rice University, Yudi Yang Rice University DOI
11:10 20m Talk		Scalable Floating-Point Satisfiability via Staged Optimization PLDI Research Papers Yuanzhuo Zhang Virginia Tech, Zhoulai Fu SUNY Korea; Virginia Tech; Stony Brook University, Binoy Ravindran Virginia Tech DOI
11:30 20m Talk		EREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination PLDI Research Papers Ekaterina Zhuchko Tallinn University of Technology, Ian Erik Varatalu Tallinn University of Technology, Margus Veanes Microsoft Research, Nikolaj Bjørner Microsoft Research DOI

10:30 - 12:10	Domain-Specific LanguagesPLDI Research Papers at Flatirons 3

10:30 20m Talk		Decoupling Data Layouts from Bounding Volume Hierarchies PLDI Research Papers Christophe Gyurgyik Stanford University, Alexander J Root Stanford University, Fredrik Kjolstad Stanford University DOI Pre-print
10:50 20m Talk		Contextual Embeddings: Implementing Bound Variables through Instance Resolution PLDI Research Papers Samantha Frohlich University of Bristol, Jessica Foster University of Bristol, Alex Kavvos University of Bristol, Meng Wang University of Bristol DOI
11:10 20m Talk		CoTenN: Constrained Optimization with Tensor Networks PLDI Research Papers Ritvik Sharma Stanford University, Cheng Peng Stanford Institute for Materials and Energy Sciences, SLAC National Accelerator Laboratory, Siddharth Dangwal University of Chicago, Sara Achour Stanford University DOI
11:30 20m Talk		Diagramming Program Values by Spatial Refinement PLDI Research Papers Siddhartha Prasad Brown University, Michael Tu Brown University, Karan Kashyap Brown University, Tim Nelson Brown University, Shriram Krishnamurthi Brown University DOI
11:50 20m Talk		Persistent Iterators with Value Semantics PLDI Research Papers Yihe Li National University of Singapore, Gregory J. Duck National University of Singapore DOI

10:30 - 12:10	Semantics and Hyperproperty ReasoningPLDI Research Papers at Flatirons 4

10:30 20m Talk		Towards Removing Undef Values from LLVM IR PLDI Research Papers Pedro Lobo INESC-ID; Instituto Superior Técnico - University of Lisbon, John McIver Virginia Tech, George Mitenkov Aptos, Juneyoung Lee AWS, Kirshanthan Sundararajah Virginia Tech, Nuno P. Lopes INESC-ID; Instituto Superior Técnico - University of Lisbon DOI Pre-print
10:50 20m Talk		The Downgrading Semantics of Memory Safety PLDI Research Papers René Rydhof Hansen Aalborg University, Andreas Stenbæk Larsen Aarhus University, Aslan Askarov Aarhus University DOI
11:10 20m Talk		Causality and Semantic Separation PLDI Research Papers Anna Zhang Massachusetts Institute of Technology, Qinglan Luo Wellesley College; Massachusetts Institute of Technology, London Bielicke University of California at Los Angeles, Eunice Jun University of California at Los Angeles, Adam Chlipala Massachusetts Institute of Technology DOI
11:30 20m Talk		Hyper Separation Logic PLDI Research Papers Trayan Gospodinov INSAIT at Sofia University St. Kliment Ohridski, Peter Müller ETH Zurich, Thibault Dardinier EPFL DOI
11:50 20m Talk		Pantomime: Constructive Leakage Proofs via Simulation PLDI Research Papers Robin Webbers Vrije Universiteit Amsterdam, Robert Schenck Northeastern University, Wind Wong Vrije Universiteit Amsterdam, Kristina Sojakova Vrije Universiteit Amsterdam, Klaus von Gleissenthall Vrije Universiteit Amsterdam DOI

13:40 - 15:00	Generative Testing and Program SynthesisPLDI Research Papers at Flatirons 2

13:40 20m Talk		[SIGPLAN] Scalable and Accurate Application-Level Crash-Consistency Testing via Representative Testing PLDI Research Papers Yile Gu University of Washington, Ian Neal University of Michigan and Veridise, Jiexiao Xu University of Washington, Shaun Christopher Lee University of Washington, Ayman Said University of Michigan, Musa Haydar University of Michigan, Jacob Van Geffen , Andrew Quinn University of California at Santa Cruz, Baris Kasikci University of Washington
14:00 20m Talk		Trace-Guided Synthesis of Effectful Test Generators PLDI Research Papers Zhe Zhou Purdue University, Ankush Desai Snowflake, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University DOI
14:20 20m Talk		Semantic Reification: A New Paradigm for Random Program Generation PLDI Research Papers Kavya Chopra ETH Zurich, Cong Li ETH Zurich, Thodoris Sotiropoulos ETH Zurich, Zhendong Su ETH Zurich DOI Pre-print
14:40 20m Talk		The Search for Constrained Random Generators PLDI Research Papers Harrison Goldstein SUNY Buffalo, Hila Peleg Technion, Cassia Torczon University of Pennsylvania, Daniel Sainati University of Pennsylvania, Leonidas Lampropoulos University of Maryland at College Park, Benjamin C. Pierce University of Pennsylvania DOI

13:40 - 15:00	Formal Verification of Probabilistic ProgramsPLDI Research Papers at Flatirons 3

13:40 20m Talk		Contextual Refinement of Higher-Order Concurrent Probabilistic Programs PLDI Research Papers Kwing Hei Li Aarhus University, Alejandro Aguirre Aarhus University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University DOI
14:00 20m Talk		Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification PLDI Research Papers Satoshi Kura Waseda University, Hiroshi Unno Tohoku University, Takeshi Tsukada Chiba University DOI
14:20 20m Talk		SuperDP: Differential Privacy Refutation via Supermartingales PLDI Research Papers Krishnendu Chatterjee IST Austria, Ehsan Kafshdar Goharshady IST Austria, Đorđe Žikelić Singapore Management University DOI
14:40 20m Talk		Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic PLDI Research Papers 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 Link to publication DOI Pre-print

13:40 - 15:00	Equality SaturationPLDI Research Papers at Flatirons 4

13:40 20m Talk		Versioned E-Graphs PLDI Research Papers Jahrim Gabriele Cesario University of St. Gallen, George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen DOI Pre-print
14:00 20m Talk		Improving Equality Saturation for EDA via Semantic E-Graphs PLDI Research Papers Sijie Kong University of California at Santa Barbara, Jingtao Xia University of California at Santa Barbara, Daniel Ruelas-Petrisko University of Washington, Zachary D. Sisco The Chinese University of Hong Kong, Shenzhen, Jonathan Balkind University of California at Santa Barbara, Gus Henry Smith Southmountain Research DOI
14:20 20m Talk		Equality Saturation for Quantum Circuit Optimization PLDI Research Papers Ganxiang Yang Columbia University, Paige Raun University of Maryland, Runzhou Tao University of Maryland, Ronghui Gu Columbia University; CertiK DOI
14:40 20m Talk		Fungible Memories for Automated Technology Mapping and Retargeting PLDI Research Papers Zachary D. Sisco The Chinese University of Hong Kong, Shenzhen, Sijie Kong University of California at Santa Barbara, Daniel Ruelas-Petrisko University of Washington, Jingtao Xia University of California at Santa Barbara, Julian Springer Technische Universität Berlin, Varun Rao University of California at Berkeley, Spencer Wang University of California at Santa Barbara, Gus Henry Smith Southmountain Research, Ben Hardekopf University of California at Santa Barbara, Jonathan Balkind University of California at Santa Barbara DOI

Fri 19 Jun
Displayed time zone: Mountain Time (US & Canada) change

09:00 - 10:10	Keynote 3PLDI Research Papers at Flatirons 2-3-4

09:00 70m Keynote		The Rise & Collapse of a Quantum State PLDI Research Papers Aws Albarghouthi University of Wisconsin-Madison

10:30 - 11:50	Static Analysis 2PLDI Research Papers at Flatirons 2

10:30 20m Talk		Verifying Array Properties in Pure Data-Parallel Programs PLDI Research Papers Nikolaj Hey Hinnerskov University of Copenhagen, Robert Schenck Northeastern University, Cosmin E. Oancea University of Copenhagen DOI
10:50 20m Talk		A Categorical Basis for Robust Program Analysis PLDI Research Papers Zachary Kincaid Princeton University, Shaowei Zhu Princeton University DOI
11:10 20m Talk		Restart and Refine: Scalable IFDS Taint Analysis across Memory Budgets PLDI Research Papers Yujiang Gui UNSW, Yonggang Tao UNSW, Jingling Xue UNSW DOI
11:30 20m Talk		Synthesizing Backward Error Bounds, Backward PLDI Research Papers Laura Zielinski Cornell University, Justin Hsu Cornell University DOI Pre-print

10:30 - 12:10	Verified Compilation and Type SystemsPLDI Research Papers at Flatirons 3

10:30 20m Talk		Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow PLDI Research Papers Zhengyao Lin Carnegie Mellon University, Yi Cai University of Maryland at College Park, Milijana Surbatovich University of Maryland at College Park DOI
10:50 20m Talk		Compiling to Recurrent Neurons PLDI Research Papers Joey Velez-Ginorio University of Pennsylvania, Nada Amin Harvard University, Konrad Kording University of Pennsylvania, Steve Zdancewic University of Pennsylvania DOI
11:10 20m Talk		[TOPLAS] Denotation-based Compositional Compiler Verification PLDI Research Papers Zhang Cheng Shanghai Jiao Tong University, Jiyang Wu , Di Wang Peking University, Qinxiang Cao Shanghai Jiao Tong University
11:30 20m Talk		Responsive Parallelism with Dynamic and First-Class Priorities PLDI Research Papers Marelle León Illinois Institute of Technology, My Dinh Illinois Institute of Technology, Stefan K. Muller University of Connecticut DOI
11:50 20m Talk		Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types PLDI Research Papers Songlin Jia Purdue University, Guannan Wei Tufts University, Siyuan He Purdue University, Yuyan Bao Augusta University, Tiark Rompf Purdue University DOI

10:30 - 12:10	Compiler Optimization for AcceleratorsPLDI Research Papers at Flatirons 4

10:30 20m Talk		Compiling Strassen-like Matrix Multiplication Algorithms to Fast CUDA Kernels PLDI Research Papers Abhinav Jangda Microsoft Research DOI
10:50 20m Talk		Parameterized Algorithms and Complexity for Function Merging with Branch Reordering PLDI Research Papers Amir K. Goharshady University of Oxford, Kerim Kochekov Hong Kong University of Science and Technology, Tian Shu Hong Kong University of Science and Technology, Ahmed Khaled Zaher Hong Kong University of Science and Technology DOI
11:10 20m Talk		NEURA: A Unified and Retargetable Compilation Framework for Coarse-Grained Reconfigurable Architectures PLDI Research Papers Shangkun Li Hong Kong University of Science and Technology, Jinming Ge Hong Kong University of Science and Technology, Diyuan Tao Independent Researcher, Zeyu Li Hong Kong University of Science and Technology, Jiawei Liang Hong Kong University of Science and Technology, Linfeng Du Hong Kong University of Science and Technology, Jiang Xu Hong Kong University of Science and Technology (Guangzhou), Wei Zhang Hong Kong University of Science and Technology, Cheng Tan Google; Arizona State University DOI
11:30 20m Talk		Neptune: Advanced ML Operator Fusion for Locality and Parallelism on GPUs PLDI Research Papers Yifan Zhao University of Illinois Urbana-Champaign, Egan Johnson University of Illinois Urbana-Champaign, Prasanth Chatarasi IBM Research, Vikram S. Adve University of Illinois Urbana-Champaign, Sasa Misailovic University of Illinois Urbana-Champaign DOI
11:50 20m Talk		SparseZETA: Intelligent Auto-tuner for Designing High-Performance SpMV Programs PLDI Research Papers Zhen Du Institute of Computing Technology at Chinese Academy of Sciences, Ying Liu Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Xionghui Chen Nanjing University, Yanbo Zhao North Carolina State University, Xiaobing Feng Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Huimin Cui Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Jiajia Li North Carolina State University DOI

13:40 - 15:20	Verification and Proof ReasoningPLDI Research Papers at Flatirons 2

13:40 20m Talk		Heterogeneous Dynamic Logic: Provability Modulo Program Theories PLDI Research Papers Samuel Teuber KIT, Mattias Ulbrich KIT, André Platzer KIT, Bernhard Beckert KIT DOI
14:00 20m Talk		Intrinsically Correct Algorithms and Recursive Coalgebras PLDI Research Papers Cass Alexandru RPTU Kaiserslautern-Landau & Radboud University Nijmegen, Henning Urbat Friedrich-Alexander University Erlangen-Nürnberg, Thorsten Wißmann Friedrich-Alexander University Erlangen-Nürnberg DOI Pre-print
14:20 20m Talk		CRIS: The Power of Imagination in Hybrid Verification PLDI Research Papers Yonghee Kim Seoul National University, Taeyoung Yoon Seoul National University, Sanghyun Yi Seoul National University, Jaehyung Lee Seoul National University, Soonwon Moon Seoul National University, Yeji Han Seoul National University, Seonho Lee Seoul National University, Taeyoung Rhee Seoul National University, Yujin Im Seoul National University, Donghyun Nam Seoul National University, Jieung Kim Yonsei University, Chung-Kil Hur Seoul National University DOI
14:40 20m Talk		Navigating AND–OR Graph Modifications to Debug Failing Proof Search PLDI Research Papers Justin Lubin University of California at Berkeley, Marlena Preigh University of California at Berkeley, Max Willsey University of California at Berkeley, Sarah E. Chasins University of California at Berkeley DOI Pre-print
15:00 20m Talk		[TOPLAS] Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software PLDI Research Papers Danel Ahman University of Tartu, Karthikeyan Bhargavan Cryspen, France, Barry Bond , Jay Bosamiya Microsoft Research, Christopher Brzuska , Antoine Delignat-Lavaud Microsoft Research, n.n., Cédric Fournet Microsoft Research, Aymeric Fromherz Inria, Sydney Gibson , Chris Hawblitzel Microsoft Research, Cătălin Hriţcu MPI-SP, Markulf Kohlweiss , Guido Martínez Microsoft Research, Haobin Ni University of Washington, Bryan Parno Carnegie Mellon University, Jonathan Protzenko Microsoft Azure Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Exequiel Rivas Tallinn University of Technology, Nikhil Swamy Microsoft Research, Santiago Zanella-Béguelin Microsoft Research, Cambridge

13:40 - 15:20	Probabilistic Inference and VerificationPLDI Research Papers at Flatirons 3

13:40 20m Talk		[SIGPLAN] Probabilistic Inference for Datalog with Correlated Inputs PLDI Research Papers Jingbo Wang Purdue University, Shashin Halalingaiah UT Austin, IIT Madras, Weiyi Chen Purdue University, Chao Wang University of Southern California, Işıl Dillig University of Texas at Austin
14:00 20m Talk		A Hierarchy of Supermartingales for ω-Regular Verification PLDI Research Papers Satoshi Kura Waseda University, Hiroshi Unno Tohoku University DOI
14:20 20m Talk		Incremental Computation for Efficient Programmable Inference in Probabilistic Programs PLDI Research Papers Fabian Zaiser Massachusetts Institute of Technology, Jack Czenszak Yale University, Martin C. Rinard Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology, Alexander K. Lew Yale University DOI
14:40 20m Talk		GradInf: Gradient Estimation as Probabilistic Inference PLDI Research Papers Gaurav Arya Carnegie Mellon University, Mathieu Huot Massachusetts Institute of Technology, Moritz Schauer Chalmers University of Technology - University of Gothenburg, Alexander K. Lew Yale University, Feras A. Saad Carnegie Mellon University DOI
15:00 20m Talk		Categorical Semantics of Probabilistic Symbolic Execution PLDI Research Papers John Li Northeastern University, Jack Czenszak Yale University, Steven Holtzen Northeastern University DOI

13:40 - 15:20	Rust Translation and BorrowingPLDI Research Papers at Flatirons 4

13:40 20m Talk		Cpp2Rust: Automatic Translation of C++ to Safe Rust PLDI Research Papers Lucian Popescu INESC-ID; Instituto Superior Técnico - University of Lisbon, Francisco Gouveia INESC-ID; Instituto Superior Técnico - University of Lisbon, Henrique Preto INESC-ID; Instituto Superior Técnico - University of Lisbon, João Silveira INESC-ID; Instituto Superior Técnico - University of Lisbon, Dmytro Hrybenko Google, José Fragoso Santos INESC-ID; Instituto Superior Técnico - University of Lisbon, Nuno P. Lopes INESC-ID; Instituto Superior Técnico - University of Lisbon DOI Pre-print
14:00 20m Talk		&inator: Correct, Precise C-to-Rust Interface Translation PLDI Research Papers Victor Chen Ohio State University, Ayden Coughlin Ohio State University, Michael D. Bond Ohio State University DOI Pre-print
14:20 20m Talk		Hayroll: A Modular Wrapper for Translating C Macros and Conditional Compilation to Rust PLDI Research Papers Haoran Peng University of Washington, Baris Kasikci University of Washington, Gilbert Louis Bernstein University of Washington, Michael D. Ernst University of Washington DOI Pre-print
14:40 20m Talk		VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type System PLDI Research Papers Travis Hance MPI-SWS, Laila Elbeheiry MPI-SWS, Yusuke Matsushita Kyoto University, Derek Dreyer MPI-SWS DOI
15:00 20m Talk		Pure Borrow: Linear Haskell Meets Rust-Style Borrowing PLDI Research Papers Yusuke Matsushita Kyoto University, Hiromi Ishii JIJ DOI Pre-print

15:50 - 17:10	Optimization of Data PipelinesPLDI Research Papers at Flatirons 2

15:50 20m Talk		[SIGPLAN] Homomorphism Calculus for User-Defined Aggregations PLDI Research Papers Ziteng Wang University of Texas at Austin, Ruijie Fang University of Texas at Austin, Linus Zheng University of Texas at Austin, Dixin Tang University of Texas at Austin, Işıl Dillig University of Texas at Austin
16:10 20m Talk		Bonsai: Compiling Queries to Pruned Tree Traversals PLDI Research Papers Alexander J Root Stanford University, Christophe Gyurgyik Stanford University, Purvi Goel Stanford University, Kayvon Fatahalian Stanford University, Jonathan Ragan-Kelley Massachusetts Institute of Technology, Andrew Adams Adobe Research, Fredrik Kjolstad Stanford University DOI Pre-print
16:30 20m Talk		A Compiler for Fused Relational Operations on Multisets PLDI Research Papers James Dong Stanford University, Fredrik Kjolstad Stanford University DOI
16:50 20m Talk		Optimal Predicate Pushdown Synthesis PLDI Research Papers Robert Zhang University of Texas at Austin, Eric Hayden Campbell University of Texas at Austin, Dixin Tang University of Texas at Austin, Işıl Dillig University of Texas at Austin DOI

15:50 - 17:10	PotpourriPLDI Research Papers at Flatirons 3

15:50 20m Talk		Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy PLDI Research Papers Eden Frenkel Tel Aviv University, Kenneth L. McMillan University of Texas at Austin, Oded Padon Weizmann Institute of Science, Sharon Shoham Tel Aviv University DOI
16:10 20m Talk		TreeCoder: Systematic Exploration and Optimisation of Decoding and Constraints for LLM Code Generation PLDI Research Papers Henrijs Princis University of Bristol, Arindam Sharma University of Bristol, Cristina David University of Bristol DOI
16:30 20m Talk		[TOPLAS] Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors PLDI Research Papers Tianchi Li Peking University, China, Zhenyu Yan Peking University, Junhao Liu Peking University, Peng Di Kunlunxin & UNSW Sydney, Xin Zhang Peking University
16:50 20m Talk		[SIGPLAN] Active Learning for Neurosymbolic Program Synthesis PLDI Research Papers Celeste Barnaby University of Texas at Austin, Jocelyn Qiaochu Chen New York University, University of Alberta, Ramya Ramalingam , Osbert Bastani University of Pennsylvania, Işıl Dillig University of Texas at Austin

15:50 - 17:10	Runtime Memory and Control AbstractionsPLDI Research Papers at Flatirons 4

15:50 20m Talk		Revisiting Partial Tracing for Safe, Efficient, and Concurrent Garbage Collection in Unmanaged Languages PLDI Research Papers Jeonghyeon Kim KAIST, Jongse Park KAIST, Youngjin Kwon KAIST, Jeehoon Kang FuriosaAI DOI Pre-print
16:10 20m Talk		Dynamically Checked Deep Immutability in Python PLDI Research Papers Fridtjof Stoldt Uppsala University, Sylvan Clebsch Microsoft Azure Research, Matthew A. Johnson Microsoft Azure Research, Matthew J. Parkinson Microsoft Azure Research, Tobias Wrigstad Uppsala University DOI
16:30 20m Talk		FlexHeap: Dynamic I/O-Aware Heap Resizing for Managed Applications PLDI Research Papers Iacovos G. Kolokasis Foundation for Research and Technology Hellas; University of Crete, Shoaib Akram Australian National University, Foivos Zakkak Red Hat, Polyvios Pratikakis Foundation for Research and Technology Hellas; University of Crete, Angelos Bilas Foundation for Research and Technology Hellas; University of Crete DOI
16:50 20m Talk		Virtualizing Continuations PLDI Research Papers Cong Ma University of Waterloo, Jonghyun Jung University of Waterloo, Yizhou Zhang University of Waterloo DOI

Unscheduled Events

	Not scheduled Talk		Soteria: Efficient Symbolic Execution as a Functional Library PLDI Research Papers Sacha-Élie Ayoun Imperial College London; Soteria Tools, Opale Sjöstedt Imperial College London; Soteria Tools, Azalea Raad Imperial College London; Soteria Tools DOI
	Not scheduled Talk		Enumerating Ill-Typed Programs for Testing Type Analyzers PLDI Research Papers Thodoris Sotiropoulos ETH Zurich, Zhendong Su ETH Zurich DOI
	Not scheduled Talk		A Verified Parallel Scheduler for OCaml 5 PLDI Research Papers Clément Allain Inria, Gabriel Scherer Inria DOI
	Not scheduled Talk		Towards Efficient Matching of Regexes with Backreferences using Register Set Automata PLDI Research Papers Vojtěch Havlena Brno University of Technology, Lukáš Holík Brno University of Technology; Aalborg University, Ondřej Lengál Brno University of Technology, Jan Vašák Brno University of Technology, Sabína Gulčíková Brno University of Technology DOI
	Not scheduled Talk		Redundant Array Computation Elimination PLDI Research Papers Zixuan Wang Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Liang Yuan Institute of Computing Technology at Chinese Academy of Sciences, Xianmeng Jiang Institute of Computing Technology at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Kun Li Institute of Computing Technology at Chinese Academy of Sciences, Junmin Xiao Institute of Computing Technology at Chinese Academy of Sciences, Yunquan Zhang Institute of Computing Technology at Chinese Academy of Sciences DOI
	Not scheduled Talk		Neuro-symbolic Hierarchical Learning for Long-Horizon Robotic Tasks PLDI Research Papers Yu Huang National University of Defense Technology, Ziji Wu National University of Defense Technology, Zhengyi Ma National University of Defense Technology, Kexin Ma National University of Defense Technology, Ji Wang National University of Defense Technology DOI
	Not scheduled Talk		Nested Inductive Types: Justified and Usable Nested Inductive Types in Lean and Rocq PLDI Research Papers Thomas Lamiaux Nantes Université; Inria, Yannick Forster Inria, Matthieu Sozeau Inria, Nicolas Tabareau Inria DOI

Accepted Papers

	Title
	Abstract Interpretation with Confidence PLDI Research Papers Yuanfeng Shi, Ziyue Jin, Xin Zhang DOI
	A Categorical Basis for Robust Program Analysis PLDI Research Papers Zachary Kincaid, Shaowei Zhu DOI
	A Compiler for Fused Relational Operations on Multisets PLDI Research Papers James Dong, Fredrik Kjolstad DOI
	A Deductive System for Contract Satisfaction Proofs PLDI Research Papers Arthur Correnson, Haoyi Zeng, Jana Hofmann DOI Pre-print
	A Formally Verified Foundation for Compositional Heterogeneous Coherence PLDI Research Papers An Qi Zhang, Andrés Goens, Daniel Sorin, Vijay Nagarajan DOI
	A Hierarchy of Supermartingales for ω-Regular Verification PLDI Research Papers Satoshi Kura, Hiroshi Unno DOI
	A Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs PLDI Research Papers Amanda Liu, Gilbert Louis Bernstein, Shoaib Kamil, Adam Chlipala, Jonathan Ragan-Kelley DOI
	Analyzing Bytes: Pre-Disassembly Static Binary Analysis PLDI Research Papers Huan Nguyen, Soumyakant Priyadarshan, Chencheng Jiang, R. Sekar DOI
	An Efficient Algorithm for Streaming BPE Tokenization PLDI Research Papers Konstantinos Mamouras, Angela W. Li, Yudi Yang DOI
	A Verified Parallel Scheduler for OCaml 5 PLDI Research Papers Clément Allain, Gabriel Scherer DOI
	Backwards-Compatible Row-Based Exceptions in ML PLDI Research Papers Simcha van Collem, Paulo Emílio de Vilhena, Robbert Krebbers DOI
	Bonsai: Compiling Queries to Pruned Tree Traversals PLDI Research Papers Alexander J Root, Christophe Gyurgyik, Purvi Goel, Kayvon Fatahalian, Jonathan Ragan-Kelley, Andrew Adams, Fredrik Kjolstad DOI Pre-print
	Bridging Coverage and Confidence: Reliable Static False Alarm Elimination via Input-Agnosticity PLDI Research Papers Jiayi Wang, Yu Wang, Linzhang Wang, Ke Wang DOI
	Categorical Semantics of Probabilistic Symbolic Execution PLDI Research Papers John Li, Jack Czenszak, Steven Holtzen DOI
	Causality and Semantic Separation PLDI Research Papers Anna Zhang, Qinglan Luo, London Bielicke, Eunice Jun, Adam Chlipala DOI
	Cerisier: A Program Logic for Attestation in a Capability Machine PLDI Research Papers June Rousseau, Denis Carnier, Thomas Van Strydonck, Steven Keuchel, Dominique Devriese, Lars Birkedal DOI
	Choose, Don’t Label: Multiple-Choice Query Synthesis for Program Disambiguation PLDI Research Papers Celeste Barnaby, Danny Ding, Osbert Bastani, Işıl Dillig DOI
	Cobble: Compiling Block Encodings for Quantum Computational Linear Algebra PLDI Research Papers Charles Yuan DOI
	Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows PLDI Research Papers 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, Peter Sewell DOI Pre-print
	Compiling Strassen-like Matrix Multiplication Algorithms to Fast CUDA Kernels PLDI Research Papers Abhinav Jangda DOI
	Compiling to Recurrent Neurons PLDI Research Papers Joey Velez-Ginorio, Nada Amin, Konrad Kording, Steve Zdancewic DOI
	Contextual Embeddings: Implementing Bound Variables through Instance Resolution PLDI Research Papers Samantha Frohlich, Jessica Foster, Alex Kavvos, Meng Wang DOI
	Contextual Refinement of Higher-Order Concurrent Probabilistic Programs PLDI Research Papers Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal DOI
	CoTenN: Constrained Optimization with Tensor Networks PLDI Research Papers Ritvik Sharma, Cheng Peng, Siddharth Dangwal, Sara Achour DOI
	Cpp2Rust: Automatic Translation of C++ to Safe Rust PLDI Research Papers Lucian Popescu, Francisco Gouveia, Henrique Preto, João Silveira, Dmytro Hrybenko, José Fragoso Santos, Nuno P. Lopes DOI Pre-print
	CRIS: The Power of Imagination in Hybrid Verification PLDI Research Papers 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 DOI
	Decoupling Data Layouts from Bounding Volume Hierarchies PLDI Research Papers Christophe Gyurgyik, Alexander J Root, Fredrik Kjolstad DOI Pre-print
	Diagramming Program Values by Spatial Refinement PLDI Research Papers Siddhartha Prasad, Michael Tu, Karan Kashyap, Tim Nelson, Shriram Krishnamurthi DOI
	Dynamically Checked Deep Immutability in Python PLDI Research Papers Fridtjof Stoldt, Sylvan Clebsch, Matthew A. Johnson, Matthew J. Parkinson, Tobias Wrigstad DOI
	Enumerating Ill-Typed Programs for Testing Type Analyzers PLDI Research Papers Thodoris Sotiropoulos, Zhendong Su DOI
	Equality Saturation for Quantum Circuit Optimization PLDI Research Papers Ganxiang Yang, Paige Raun, Runzhou Tao, Ronghui Gu DOI
	EREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination PLDI Research Papers Ekaterina Zhuchko, Ian Erik Varatalu, Margus Veanes, Nikolaj Bjørner DOI
	Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types PLDI Research Papers Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao, Tiark Rompf DOI
	Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation PLDI Research Papers Shaurya Gomber, Debangshu Banerjee, Gagandeep Singh DOI Pre-print
	Expecto: Extracting Formal Specifications from Natural Language Description for Trustworthy Oracles PLDI Research Papers Dongjae Lee, Kihong Heo DOI
	Exploiting Sophisticated Static Analysis for Verilog PLDI Research Papers Qinlin Chen, Nairen Zhang, Jinpeng Wang, Jiacai Cui, Tian Tan, Xiaoxing Ma, Chang Xu, Jian Lu, Yue Li DOI
	Fast Atomicity Monitoring PLDI Research Papers Hünkar Can Tunç, Yifan Dong, Andreas Pavlogiannis DOI
	Fixed Parameter Tractable Linearizability Monitoring PLDI Research Papers Zheng Han Lee, Umang Mathur DOI Pre-print
	FlexHeap: Dynamic I/O-Aware Heap Resizing for Managed Applications PLDI Research Papers Iacovos G. Kolokasis, Shoaib Akram, Foivos Zakkak, Polyvios Pratikakis, Angelos Bilas DOI
	Flow-Analysis-Based Closure Optimization PLDI Research Papers John Reppy, Olin Shivers, Byron Zhong DOI
	Fungible Memories for Automated Technology Mapping and Retargeting PLDI Research Papers Zachary D. Sisco, Sijie Kong, Daniel Ruelas-Petrisko, Jingtao Xia, Julian Springer, Varun Rao, Spencer Wang, Gus Henry Smith, Ben Hardekopf, Jonathan Balkind DOI
	GradInf: Gradient Estimation as Probabilistic Inference PLDI Research Papers Gaurav Arya, Mathieu Huot, Moritz Schauer, Alexander K. Lew, Feras A. Saad DOI
	Hayroll: A Modular Wrapper for Translating C Macros and Conditional Compilation to Rust PLDI Research Papers Haoran Peng, Baris Kasikci, Gilbert Louis Bernstein, Michael D. Ernst DOI Pre-print
	Heterogeneous Dynamic Logic: Provability Modulo Program Theories PLDI Research Papers Samuel Teuber, Mattias Ulbrich, André Platzer, Bernhard Beckert DOI
	Hybrid Path-Sums for Hybrid Quantum Programs PLDI Research Papers Christopĥe Chareton, Sébastien Bardin, Jad Issa, Mathieu Nguyen, Nicolas Blanco DOI
	Hyper Separation Logic PLDI Research Papers Trayan Gospodinov, Peter Müller, Thibault Dardinier DOI
	Implementability of Global Distributed Protocols Modulo Network Architectures PLDI Research Papers Elaine Li, Thomas Wies DOI
	Improving Equality Saturation for EDA via Semantic E-Graphs PLDI Research Papers Sijie Kong, Jingtao Xia, Daniel Ruelas-Petrisko, Zachary D. Sisco, Jonathan Balkind, Gus Henry Smith DOI
	&inator: Correct, Precise C-to-Rust Interface Translation PLDI Research Papers Victor Chen, Ayden Coughlin, Michael D. Bond DOI Pre-print
	Incremental Computation for Efficient Programmable Inference in Probabilistic Programs PLDI Research Papers Fabian Zaiser, Jack Czenszak, Martin C. Rinard, Vikash K. Mansinghka, Alexander K. Lew DOI
	Intrinsically Correct Algorithms and Recursive Coalgebras PLDI Research Papers Cass Alexandru, Henning Urbat, Thorsten Wißmann DOI Pre-print
	Iris-WasmFX: Modular Reasoning for Wasm Stack Switching PLDI Research Papers Maxime Legoupil, Mathias Pedersen, Lars Birkedal, Sam Lindley, Jean Pichon-Pharabod DOI
	Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic PLDI Research Papers Guido Martínez, Bastian Köpcke, Jonáš Fiala, Gabriel Ebner, Tahina Ramananandro, Michel Steuwer, Tyler Sorensen, Nikhil Swamy DOI
	Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow PLDI Research Papers Zhengyao Lin, Yi Cai, Milijana Surbatovich DOI
	MatchBox: A Semantic Foundation for Data Plane Portability PLDI Research Papers Eric Hayden Campbell, Robert Zhang, Divyanshu Saxena, Aditya Akella, Işıl Dillig DOI
	Modular GPU Programming with Typed Perspectives PLDI Research Papers Manya Bansal, Daniel Sainati, Joseph W. Cutler, Saman Amarasinghe, Jonathan Ragan-Kelley DOI
	Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic PLDI Research Papers Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen, Kwing Hei Li, Joseph Tassarotti, Lars Birkedal Link to publication DOI Pre-print
	Navigating AND–OR Graph Modifications to Debug Failing Proof Search PLDI Research Papers Justin Lubin, Marlena Preigh, Max Willsey, Sarah E. Chasins DOI Pre-print
	Neptune: Advanced ML Operator Fusion for Locality and Parallelism on GPUs PLDI Research Papers Yifan Zhao, Egan Johnson, Prasanth Chatarasi, Vikram S. Adve, Sasa Misailovic DOI
	Nested Inductive Types: Justified and Usable Nested Inductive Types in Lean and Rocq PLDI Research Papers Thomas Lamiaux, Yannick Forster, Matthieu Sozeau, Nicolas Tabareau DOI
	NEURA: A Unified and Retargetable Compilation Framework for Coarse-Grained Reconfigurable Architectures PLDI Research Papers Shangkun Li, Jinming Ge, Diyuan Tao, Zeyu Li, Jiawei Liang, Linfeng Du, Jiang Xu, Wei Zhang, Cheng Tan DOI
	Neuro-symbolic Hierarchical Learning for Long-Horizon Robotic Tasks PLDI Research Papers Yu Huang, Ziji Wu, Zhengyi Ma, Kexin Ma, Ji Wang DOI
	Optimal Predicate Pushdown Synthesis PLDI Research Papers Robert Zhang, Eric Hayden Campbell, Dixin Tang, Işıl Dillig DOI
	Optimism in Equality Saturation PLDI Research Papers Russel Arbore, Alvin Cheung, Max Willsey DOI Pre-print
	Pantomime: Constructive Leakage Proofs via Simulation PLDI Research Papers Robin Webbers, Robert Schenck, Wind Wong, Kristina Sojakova, Klaus von Gleissenthall DOI
	Parameterized Algorithms and Complexity for Function Merging with Branch Reordering PLDI Research Papers Amir K. Goharshady, Kerim Kochekov, Tian Shu, Ahmed Khaled Zaher DOI
	Path-Sensitive Abstract Interpretation for WCET Estimation PLDI Research Papers Shangshang Xiao, Mengxia Sun, Wei Zhang, Naijun Zhan, Lei Ju DOI
	Persistent Iterators with Value Semantics PLDI Research Papers Yihe Li, Gregory J. Duck DOI
	Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics PLDI Research Papers Rui Dong, Qingyue Wu, Danny Ding, Zheng Guo, Ruyi Ji, Xinyu Wang DOI
	Pure Borrow: Linear Haskell Meets Rust-Style Borrowing PLDI Research Papers Yusuke Matsushita, Hiromi Ishii DOI Pre-print
	Redundant Array Computation Elimination PLDI Research Papers Zixuan Wang, Liang Yuan, Xianmeng Jiang, Kun Li, Junmin Xiao, Yunquan Zhang DOI
	Responsive Parallelism with Dynamic and First-Class Priorities PLDI Research Papers Marelle León, My Dinh, Stefan K. Muller DOI
	Restart and Refine: Scalable IFDS Taint Analysis across Memory Budgets PLDI Research Papers Yujiang Gui, Yonggang Tao, Jingling Xue DOI
	Revisiting Partial Tracing for Safe, Efficient, and Concurrent Garbage Collection in Unmanaged Languages PLDI Research Papers Jeonghyeon Kim, Jongse Park, Youngjin Kwon, Jeehoon Kang DOI Pre-print
	SAIL: Sound Abstract Interpreters with LLMs PLDI Research Papers Qiuhan Gu, Avaljot Singh, Gagandeep Singh DOI
	SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits PLDI Research Papers Nengkun Yu, Jens Palsberg, Thomas Reps DOI
	Scalable Floating-Point Satisfiability via Staged Optimization PLDI Research Papers Yuanzhuo Zhang, Zhoulai Fu, Binoy Ravindran DOI
	Semantic Reification: A New Paradigm for Random Program Generation PLDI Research Papers Kavya Chopra, Cong Li, Thodoris Sotiropoulos, Zhendong Su DOI Pre-print
	Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy PLDI Research Papers Eden Frenkel, Kenneth L. McMillan, Oded Padon, Sharon Shoham DOI
	SIMT-Step Execution: A Flexible Operational Semantics For GPU Subgroup Behavior PLDI Research Papers Zheyuan Chen, Naomi Rehman, Guido Martínez, Tyler Sorensen DOI
	Solvable Tuple Patterns and Their Applications to Program Verification PLDI Research Papers Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, Ryo Yoshinaka DOI
	Soteria: Efficient Symbolic Execution as a Functional Library PLDI Research Papers Sacha-Élie Ayoun, Opale Sjöstedt, Azalea Raad DOI
	SparseZETA: Intelligent Auto-tuner for Designing High-Performance SpMV Programs PLDI Research Papers Zhen Du, Ying Liu, Xionghui Chen, Yanbo Zhao, Xiaobing Feng, Huimin Cui, Jiajia Li DOI
	SSA without Dominance for Higher-Order Programs PLDI Research Papers Roland Leißa, Johannes Griebler DOI Pre-print
	State Space Estimation for DPOR-Based Model Checkers PLDI Research Papers A. R. Balasubramanian, Mohammad Hossein Khoshechin Jorshari, Rupak Majumdar, Umang Mathur, Minjian Zhang DOI Pre-print
	SuperCollider: Scalable and Effective Data Race Detection for CUDA PLDI Research Papers Mark Stephenson, Sana Damani, Mohamed Tarek Ibn Ziad, Anis Ladram, Michael Garland DOI
	SuperDP: Differential Privacy Refutation via Supermartingales PLDI Research Papers Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Đorđe Žikelić DOI
	Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification PLDI Research Papers Satoshi Kura, Hiroshi Unno, Takeshi Tsukada DOI
	SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine Protocols PLDI Research Papers Longfei Qiu, Jingqi Xiao, Ji-Yong Shin, Zhong Shao DOI
	Syntactic Implicit Parameters with Static Overloading PLDI Research Papers Daan Leijen, Tim Whiting DOI Pre-print
	Synthesizing Backward Error Bounds, Backward PLDI Research Papers Laura Zielinski, Justin Hsu DOI Pre-print
	The Downgrading Semantics of Memory Safety PLDI Research Papers René Rydhof Hansen, Andreas Stenbæk Larsen, Aslan Askarov DOI
	The Search for Constrained Random Generators PLDI Research Papers Harrison Goldstein, Hila Peleg, Cassia Torczon, Daniel Sainati, Leonidas Lampropoulos, Benjamin C. Pierce DOI
	Towards Efficient Matching of Regexes with Backreferences using Register Set Automata PLDI Research Papers Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Jan Vašák, Sabína Gulčíková DOI
	Towards Removing Undef Values from LLVM IR PLDI Research Papers Pedro Lobo, John McIver, George Mitenkov, Juneyoung Lee, Kirshanthan Sundararajah, Nuno P. Lopes DOI Pre-print
	Trace-Guided Synthesis of Effectful Test Generators PLDI Research Papers Zhe Zhou, Ankush Desai, Benjamin Delaware, Suresh Jagannathan DOI
	TreeCoder: Systematic Exploration and Optimisation of Decoding and Constraints for LLM Code Generation PLDI Research Papers Henrijs Princis, Arindam Sharma, Cristina David DOI
	Typestate via Revocable Capabilities PLDI Research Papers Songlin Jia, Craig Liu, Siyuan He, Haotian Deng, Yuyan Bao, Tiark Rompf DOI
	Uniformity Analysis in the WebGPU Shading Language PLDI Research Papers James Lee-Jones, John Wickerson, Alastair F. Donaldson DOI
	Verification Modulo Tested Library Contracts PLDI Research Papers Abhishek Uppar, Omar Muhammad, Sumanth Prabhu S, Deepak D'Souza, P. Madhusudan, Adithya Murali DOI
	Verification of Recursively Defined Quantum Circuits PLDI Research Papers Mingsheng Ying, Zhicheng Zhang DOI
	Verifying Array Properties in Pure Data-Parallel Programs PLDI Research Papers Nikolaj Hey Hinnerskov, Robert Schenck, Cosmin E. Oancea DOI
	Versioned E-Graphs PLDI Research Papers Jahrim Gabriele Cesario, George Zakhour, Pascal Weisenburger, Guido Salvaneschi DOI Pre-print
	VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type System PLDI Research Papers Travis Hance, Laila Elbeheiry, Yusuke Matsushita, Derek Dreyer DOI
	Virtualizing Continuations PLDI Research Papers Cong Ma, Jonghyun Jung, Yizhou Zhang DOI
	Weighted NetKAT: A Programming Language For Quantitative Network Verification PLDI Research Papers Emmanuel Suárez Acevedo, Tiago Ferreira, Kevin Batz, Oliver Emil Bøving, Nate Foster, Alexandra Silva DOI

Call for Papers

PACMPL Issue PLDI 2026 seeks contributions on all aspects of programming languages research, broadly construed, including design, implementation, theory, applications, and performance.

Authors of papers published in PACMPL Issue PLDI 2026 will be invited – but not required – to present their work in the PLDI conference in June 2026, which is sponsored by ACM SIGPLAN.

NEW FOR 2026: authors will be asked whether they intend to submit an artifact as part of the paper submission process; see Artifact Evaluation and Artifact Intent below.

Scope

PLDI is a premier forum for programming language research, broadly construed. Outstanding research that extends and/or applies programming-language concepts to advance the field of computing is welcome. Novel system designs, thorough empirical work, well-motivated theoretical results, and new application areas are all in scope for PLDI. Papers demonstrating significant industrial application and large-scale evaluation of PL techniques are welcome.

Evaluation Criteria and Process

Reviewers will evaluate submissions for accuracy, significance, originality, and clarity. Submissions should be organized to communicate clearly to a broad programming-language audience as well as experts on the paper’s topics. Papers should identify what has been accomplished and how it relates to previous work. Authors of empirical papers are encouraged to consider the seven categories of the SIGPLAN Empirical Evaluation Guidelines when preparing submissions.

The selection of papers will be made in two rounds of reviewing. In the first round, reviewers will assess the papers according to the quality criteria listed above. Authors will be given several days to compose a written response to the reviews received in the first round – e.g., to correct errors and clarify technical concerns. At the end of the first round, the Review Committee will conditionally accept a subset of the submissions and all other submissions will be rejected. In the second round, authors of conditionally-accepted papers will be given an opportunity to improve specific aspects of the research and the paper, as identified by the reviewers. Authors will have sufficient time to perform the required revisions and re-submit the paper. The same reviewers as in the first round will then assess how the revision requests have been acted upon by the authors. Revisions that fail to adequately address the reviewers’ original concerns will result in rejection.

The Review Committee will make final decisions regarding (conditional) acceptance and rejection, although reviews for a given paper will typically be performed by a subset of the committee. During the review period, authors must not contact Review Committee members – all questions must be addressed to the Associate Editor (who is doing the job that we would have called “Program Chair” before PLDI joined PACMPL). Contacting Review Committee members about submitted paper(s) is an ethical violation and may be grounds for summary rejection.

Deadlines and formatting requirements, detailed below, will be strictly enforced.

Double-Blind Reviewing

Author names and affiliations must be omitted from submissions. If a submission refers to prior work done by the authors, that reference should be made in third person. Any supplementary material must also be anonymized. These are firm submission requirements. The Review Committee will only learn the identities of authors of accepted papers following the second round of reviewing.

The FAQ on Double-Blind Reviewing clarifies the policy for the most common scenarios. But there are many gray areas and trade-offs. If you have any doubts about how to interpret the double-blind rules, or any cases that are not fully covered by the FAQ, please contact the Associate Editor. In complex cases, it is better to get guidance from the Associate Editor than to risk summary rejection.

Submission Site Information

The submission site is https://pldi2026.hotcrp.com.

Authors can submit multiple times prior to the (firm!) deadline. Only the last submission will be reviewed. There is no deadline for submitting abstracts. The submission site requires entering author names and affiliations, relevant topics, and potential conflicts. Addition or removal of authors after the submission deadline will need to be approved by the Associate Editor (as this kind of change potentially undermines the goal of eliminating conflicts during paper assignment).

The submission deadline is 11:59PM on Thursday November 13, 2025 anywhere on earth: https://en.wikipedia.org/wiki/Anywhere_on_Earth

Declaring Conflicts

When submitting a paper, you will need to declare potential conflicts. Conflicts should be declared between an adviser and an advisee (e.g., Ph.D., post-doc). Other conflicts include institutional conflicts, financial conflicts of interest, friends or relatives, or any recent co-authors on papers and proposals (last 2 years).

Please do not declare spurious conflicts: such incorrect conflicts are especially harmful if the aim is to subvert the normal peer-review process by excluding potential reviewers. Listing spurious conflicts can be grounds for rejection. If you are unsure about whether or not a given relationship constitutes a conflict, please consult the Associate Editor.

Formatting Requirements

Each paper should have no more than 20 pages of text, excluding bibliography, using the ACM Proceedings format. This format is chosen for compatibility with PACMPL. It is a single-column page layout with a 10 pt font, 12 pt line spacing, and wider margins than recent PLDI page layouts. In this format, the main text block is 5.478 in (13.91 cm) wide and 7.884 in (20.03 cm) tall. Use of a different format (e.g., smaller fonts or a larger text block) is grounds for summary rejection. PACMPL templates for Microsoft Word and LaTeX can be found at the SIGPLAN author information page. Authors using LaTeX should use the sample-acmsmall-conf.tex file (found in the samples folder of the acmart package) with the acmsmall option. We also strongly encourage use of the review and screen options as well, e.g.:

\documentclass[acmsmall,screen,review,anonymous,nonacm]{acmart}

Papers may be submitted using either author-year or numeric format for citations. Submissions should be in PDF and printable on both US Letter and A4 paper. Please take care to ensure that figures and tables are legible, even when the paper is printed in gray-scale. Papers that exceed the length requirement, deviate from the expected format, or are submitted late will be rejected.

Supplementary Material

Authors are welcome to provide supplementary material if that material supports the claims in the paper. Such material may include proofs, experimental results, and/or data sets. This material should be uploaded at the same time as the submission. Reviewers are not required to examine the supplementary material but may refer to it if they would like to find further evidence supporting the claims in the paper. All supplementary material must be anonymized.

Supplemental material cannot be included in the main submission text. All appendices must be submitted as supplemental material, not as part of the main submission PDF.

Plagiarism and Concurrent Work

Papers must describe unpublished work that is not currently submitted for publication elsewhere, as described by the SIGPLAN Republication Policy and ACM Policy on Plagiarism. Concurrent submissions to other conferences, workshops, journals, or similar venues of publication are disallowed. Prior work must, as always, be cited and referred to in the third person even if it is the authors’ own work, so as to preserve author anonymity. If you have further questions, please contact the Associate Editor.

Artifact Evaluation and Artifact Intent

Authors of accepted papers will be invited to submit supporting materials to the Artifact Evaluation process. Artifact Evaluation is run by a separate committee whose task is to assess how well the artifacts support the work described in the papers. At artifact submission time, authors will be asked to provide an artifact availability statement that details the expected behavior of the artifact, and how it pertains to the results of the paper. Artifact submission is voluntary but encouraged. The results of the artifact evaluation process will not influence the final decision regarding the papers.

Papers that go through the Artifact Evaluation process successfully will receive a badge printed on the papers themselves, and include the artifact availability statement (which will not count agains the page limit). Authors of accepted papers are encouraged to make their artifacts publicly available upon publication of the proceedings, by including them as “source materials” in the ACM Digital Library.

NEW FOR 2026: At paper submission time, authors will be asked whether they intend to submit an artifact for evaluation, and to provide an explanation if they do not intend to do so. (It is recognized that artifacts may not be appropriate for all papers, and they are still not required.) Information on artifact intent for a submission will be shared with reviewers, but the artifact evaluation process remains independent of the process for deciding paper acceptance. If authors indicate they intend to submit an artifact but do not do so after conditional acceptance, they will be asked to explain the discrepancy.

Open Access and Copyright

As a Gold Open Access journal, PACMPL is committed to making peer-reviewed scientific research free of restrictions on both access and (re-)use. Authors are strongly encouraged to support liberal open access by licensing their work with the Creative Commons Attribution 4.0 International (CC BY) license, which grants readers (re-)use rights.

Authors of accepted papers will be required to provide an ORCID for each co-author and choose one of the following publication rights:
Author licenses the work with a Creative Commons license, retains copyright, and (implicitly) grants ACM non-exclusive permission to publish (suggested choice).
Author retains copyright of the work and grants ACM a non-exclusive permission to publish license.
Author retains copyright of the work and grants ACM an exclusive permission to publish license.
Author transfers copyright of the work to ACM.

Publication Date

All papers will be archived by the ACM Digital Library. Authors will have the option of including supplementary material with their paper. The official publication date is the date the proceedings are made available in the ACM Digital Library or the first day of the conference, which ever is sooner. Note that the date may be up to two weeks prior to the first day of the conference. The official publication date affects the deadline for any patent filings related to published work.

Important update on ACMs new open access publishing model for 2026 ACM Conferences:

Starting January 1, 2026, ACM will fully transition to Open Access. All ACM publications, including those from ACM-sponsored conferences, will be 100% Open Access. Authors will have two primary options for publishing Open Access articles with ACM: the ACM Open institutional model or by paying Article Processing Charges (APCs). With over 1,800 institutions already part of ACM Open, the majority of ACM-sponsored conference papers will not require APCs from authors or conferences (currently, around 70-75%).

Authors from institutions not participating in ACM Open will need to pay an APC to publish their papers, unless they qualify for a geographic or discretionary waiver. To find out whether an APC applies to your article, please consult the list of participating institutions in ACM Open and review the APC Waivers and Discounts Policy. Note: to be eligible for the ACM Open option, the corresponding author for an article must be affiliated with an ACM Open institution.

To support a smooth transition and encourage broader ACM Open participation, ACM has introduced a temporary subsidy on APC pricing for 2026, funded directly by ACM. This pricing applies to all articles published in ACM and SIG sponsored conferences taking place in 2026. The subsidized conference pricing for 2026 is as follows:

Authors	No ACM or SIG members	At least 1 ACM or SIG member
ACM and SIG Sponsored Conference Article	$350	$250
From a lower-middle-income country	$175	$125

This represents a 65% discount, funded directly by ACM. Authors are encouraged to help advocate for their institutions to join ACM Open during this transition period.

Presentations

Authors of accepted papers will be invited to present their work at PLDI. Authors who need financial assistance for travel to the conferences should apply for a grant from the SIGPLAN Professional Activities Committee (PAC) program. We welcome all authors, regardless of nationality. If authors are not able to obtain visas to travel to the conference despite making reasonable effort, we will make arrangements to facilitate remote participation or presentation by another attendee on behalf of the authors.

Distinguished Paper Awards

Up to 10% of the accepted papers may be designated as Distinguished Papers. This award highlights papers that the Review Committee believes should be read by a broad audience due to their relevance, originality, significance, and clarity. The set of distinguished papers will be chosen through a rigorous review process of the final papers, carried out by a subset of the Review Committee.

Acknowledgments

This call-for-papers is an adaptation and evolution of content from previous SIGPLAN conferences. We are grateful to prior organizers for their work, which is reused here.

Code of Conduct

PLDI follows the ACM Policy Against Harassment at ACM Activities. Please familiarize yourself with the policy and guide for reporting unacceptable behavior.

PLDI Research Papers

This program is tentative and subject to change.

Program Display Configuration

Wed 17 JunDisplayed time zone: Mountain Time (US & Canada) change

Thu 18 JunDisplayed time zone: Mountain Time (US & Canada) change

Fri 19 JunDisplayed time zone: Mountain Time (US & Canada) change

Unscheduled Events

Accepted Papers

Call for Papers

FAQ on Double-Blind Reviewing

Manu SridharanChair

University of California at Riverside

United States

Satish ChandraAssociate Chair

Meta Platforms, Inc.

United States

Derek DreyerAssociate Chair

MPI-SWS

Germany

Sophia DrossopoulouAssociate Chair

Imperial College London

United Kingdom

Jeffrey S. FosterAssociate Chair

Tufts University

United States

David GroveAssociate Chair

IBM Research

United States

Ruzica PiskacAssociate Chair

Yale University

United States

John RegehrAssociate Chair

University of Utah

United States

Adrian SampsonAssociate Chair

Cornell University

Zhendong SuAssociate Chair

ETH Zurich

Switzerland

Parosh Aziz Abdulla

Uppsala University; Mälardalen University

Sweden

Coşku Acay

Observe, Inc.

United States

Sara Achour

Stanford University

United States

Michael D. Adams

National University of Singapore

United States

Jonathan Aldrich

Carnegie Mellon University

United States

Haniel Barbosa

Universidade Federal de Minas Gerais

Brazil

Sébastien Bardin

CEA List - Université Paris-Saclay

France

Rohan Bavishi

Amazon

United States

Gilbert Louis Bernstein

University of Washington

United States

Ivan Beschastnikh

The University of British Columbia

Canada

Pramod Bhatotia

TU Munich

Germany

Rastislav Bodík

Google Research, Brain Team

United States

Michael D. Bond

Ohio State University

United States

Ahmed Bouajjani

IRIF, Université Paris Diderot

Wed 17 Jun
Displayed time zone: Mountain Time (US & Canada) change

Thu 18 Jun
Displayed time zone: Mountain Time (US & Canada) change

Fri 19 Jun
Displayed time zone: Mountain Time (US & Canada) change