PLDI 2024
Mon 24 - Fri 28 June 2024 Copenhagen, Denmark
Dates
Plenary

This program is tentative and subject to change.

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

Wed 26 Jun

Displayed time zone: Windhoek change

09:00 - 10:10
09:00 - 10:10
10:40 - 12:20
Probabilistic ProgrammingPLDI Research Papers at Finland / Norway
10:40
20m
Talk
Bit Blasting Probabilistic Programs
PLDI Research Papers
Poorva Garg University of California, Los Angeles, Steven Holtzen Northeastern University, Guy Van den Broeck University of California at Los Angeles, Todd Millstein University of California at Los Angeles
DOI
11:00
20m
Talk
Compiling Probabilistic Programs for Variable Elimination with Information Flow
PLDI Research Papers
Jianlin Li University of Waterloo, Eric Wang University of Waterloo, Yizhou Zhang University of Waterloo
DOI
11:20
20m
Talk
Equivalence and Similarity Refutation for Probabilistic Programs
PLDI Research Papers
Krishnendu Chatterjee IST Austria, Ehsan Kafshdar Goharshady IST Austria, Petr Novotný Masaryk University, Đorđe Žikelić Singapore Management University, Singapore
DOI
11:40
20m
Talk
GenSQL: A Probabilistic Programming System for Querying Generative Models of Database Tables
PLDI Research Papers
Mathieu Huot MIT, Matin Ghavami Massachusetts Institute of Technology, Alexander K. Lew Massachusetts Institute of Technology, Ulrich Schaechtle Digital Garage, Cameron Freer Massachusetts Institute of Technology, Zane Shelby Digital Garage, Martin Rinard MIT, Feras Saad Carnegie Mellon University, Vikash K. Mansinghka Massachusetts Institute of Technology
DOI
12:00
20m
Talk
Probabilistic Programming with Programmable Variational Inference
PLDI Research Papers
McCoy Reynolds Becker MIT, Alexander K. Lew Massachusetts Institute of Technology, Xiaoyan Wang Massachusetts Institute of Technology, Matin Ghavami Massachusetts Institute of Technology, Mathieu Huot MIT, Martin Rinard MIT, Vikash K. Mansinghka Massachusetts Institute of Technology
DOI
10:40 - 12:20
10:40
20m
Talk
Compilation of Qubit Circuits to Optimized Qutrit Circuits
PLDI Research Papers
Ritvik Sharma Stanford University, Sara Achour Stanford University
DOI
11:00
20m
Talk
Qubit Recycling Revisited
PLDI Research Papers
Hanru Jiang Beijing Institute of Mathematical Sciences and Applications
DOI
11:20
20m
Talk
The T-Complexity Costs of Error Correction for Control Flow in Quantum Computation
PLDI Research Papers
Charles Yuan Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
DOI
11:40
20m
Talk
Symbolic Execution for Quantum Error Correction Programs
PLDI Research Papers
Wang Fang Institute of Software at Chinese Academy of Sciences and University of Chinese Academy of Sciences, Mingsheng Ying Institute of Software at Chinese Academy of Sciences; Tsinghua University
DOI
12:00
20m
Talk
An Algebraic Language for Specifying Quantum Networks
PLDI Research Papers
Anita Buckley USI Lugano, Pavel Chuprikov USI Lugano, Rodrigo Otoni USI Lugano, Robert Soulé Yale University, Robert Rand University of Chicago, Patrick Eugster USI Lugano; Purdue University
DOI
10:40 - 12:20
Parsing and Compiling and Transforming PLDI Research Papers at Sweden
10:40
20m
Talk
Daedalus: Safer Document Parsing
PLDI Research Papers
Iavor Diatchki Galois, Inc., Mike Dodds Galois, Inc., Harrison Goldstein University of Pennsylvania, Bill Harris Galois, David Holland Galois, Benoit Razet Galois, Inc, Cole Schlesinger Galois, Simon Winwood Galois
DOI
11:00
20m
Talk
SpEQ: Translation of Sparse Codes using Equivalences
PLDI Research Papers
Avery Laird University of Toronto, Bangtian Liu University of Toronto, Nikolaj Bjørner Microsoft Research, Maryam Mehri Dehnavi University of Toronto
DOI Pre-print
11:20
20m
Talk
A Lightweight Polyglot Code Transformation Language
PLDI Research Papers
Ameya Ketkar Gitar, Daniel Ramos Carnegie Mellon University, and INESC-ID, Lazaro Clapp Gitar, Raj Barik Gitar Co., Murali Krishna Ramanathan AWS AI Labs
DOI Pre-print
11:40
20m
Talk
Compiling with Abstract Interpretation
PLDI Research Papers
Dorian Lesbre CEA List, Matthieu Lemerre Université Paris-Saclay - CEA LIST
DOI
12:00
20m
Talk
Don’t Write, but Return: Replacing Output Parameters with Algebraic Data Types in C-to-Rust Translation
PLDI Research Papers
DOI
12:20 - 13:40
13:40 - 15:20
13:40
20m
Talk
Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
PLDI Research Papers
Peixin Wang University of Oxford, Tengshun Yang SKLCS, Institute of Software, Chinese Academy of Sciences & University of Chinese Academy of Sciences, Hongfei Fu Shanghai Jiao Tong University, Guanyan Li University of Oxford, C.-H. Luke Ong NTU
DOI
14:00
20m
Talk
Compiling Conditional Quantum Gates without Using Helper Qubits
PLDI Research Papers
Keli Huang University of California at Los Angeles, Jens Palsberg University of California, Los Angeles (UCLA)
DOI
14:20
20m
Talk
Consolidating Smart Contracts with Behavioral Contracts
PLDI Research Papers
Guannan Wei Purdue University, Danning Xie Purdue University, Wuqi Zhang The Hong Kong University of Science and Technology, Yongwei Yuan Purdue University, Zhuo Zhang Purdue University
DOI
14:40
20m
Talk
NetBlocks: Staging Layouts for High-Performance Custom Host Network Stacks
PLDI Research Papers
Ajay Brahmakshatriya Massachusetts Institute of Technology, Christopher Rinard Massachusetts Institute of Technology, Manya Ghobadi Massachusetts Institute of Technology, Saman Amarasinghe Massachusetts Institute of Technology
DOI
15:00
20m
Talk
KATch: A Fast Symbolic Verifier for NetKAT
PLDI Research Papers
Mark Moeller Cornell University, Jules Jacobs Cornell University, Olivier Savary Bélanger Galois, Inc., David Darais Galois, Cole Schlesinger Galois, Steffen Smolka Google, Nate Foster Cornell University and Jane Street, Alexandra Silva Cornell University
DOI
13:40 - 15:20
Formal Verification 1PLDI Research Papers at Iceland / Denmark
13:40
20m
Talk
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language
PLDI Research Papers
Gaurav Parthasarathy ETH Zurich, Thibault Dardinier ETH Zurich, Benjamin Bonneau Verimag, Peter Müller ETH Zurich, Alexander J. Summers University of British Columbia
DOI
14:00
20m
Talk
Verified Extraction from Coq to OCaml
PLDI Research Papers
DOI
14:20
20m
Talk
Verification under Intel-x86 with Persistency
PLDI Research Papers
Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Ahmed Bouajjani IRIF, Université Paris Diderot, K Narayan Kumar Chennai Mathematical Institute, Prakash Saivasan The Institute of Mathematical Sciences, India
DOI
14:40
20m
Talk
RefinedRust: A Type System for High-Assurance Verification of Rust Programs
PLDI Research Papers
Lennard Gäher MPI-SWS, Michael Sammler MPI-SWS, Ralf Jung ETH Zurich, Robbert Krebbers Radboud University Nijmegen, Derek Dreyer MPI-SWS
DOI
15:00
20m
Talk
Hyperblock Scheduling for Verified High-Level Synthesis
PLDI Research Papers
Yann Herklotz Imperial College London, John Wickerson Imperial College London
DOI Pre-print
13:40 - 15:20
Types and EffectsPLDI Research Papers at Sweden
13:40
20m
Talk
Space-Efficient Polymorphic Gradual Typing, Mostly Parametric
PLDI Research Papers
Atsushi Igarashi Kyoto University, Shota Ozaki Kyoto University, Taro Sekiyama National Institute of Informatics, Yudai Tanabe Tokyo Institute of Technology
DOI
14:00
20m
Talk
Associated Effects
PLDI Research Papers
Matthew Lutze Aarhus University, Magnus Madsen Aarhus University
DOI
14:20
20m
Talk
Decidable Subtyping of Existential Types for Julia
PLDI Research Papers
Julia Belyakova Purdue University, Benjamin Chung Northeastern University, Ross Tate Independent Consultant, Jan Vitek Northeastern University
DOI
14:40
20m
Talk
Numerical Fuzz: A Type System for Rounding Error Analysis
PLDI Research Papers
Ariel E. Kellison Cornell University, Justin Hsu Cornell University
DOI
15:00
20m
Talk
Stream Types
PLDI Research Papers
Joseph W. Cutler University of Pennsylvania, Chris Watson University of Pennsylvania, Emeka Nkurumeh California Institute of Technology, Phillip Hilliard University of Pennsylvania, Harrison Goldstein University of Pennsylvania, Caleb Stanford University of California, Davis, Benjamin C. Pierce University of Pennsylvania
DOI
16:00 - 17:20
Security and CryptographyPLDI Research Papers at Finland / Norway
16:00
20m
Talk
A Tensor Compiler with Automatic Data Packing for Simple and Efficient Fully Homomorphic Encryption
PLDI Research Papers
Nikola Samardzic Massachusetts Institute of Technology, Aleksandar Krastev Massachusetts Institute of Technology, Simon Langowski Massachusetts Institute of Technology, Srinivas Devadas Massachusetts Institute of Technology, Daniel Sanchez MIT
DOI
16:20
20m
Talk
Quantitative Robustness for Vulnerability Assessment
PLDI Research Papers
Guillaume Girol CEA, List, Université Paris Saclay, Guilhem Lacombe CEA LIST and Université Paris-Saclay, Sébastien Bardin CEA LIST, University Paris-Saclay
DOI
16:40
20m
Talk
Quest Complete: The Holy Grail of Gradual Security
PLDI Research Papers
Tianyu Chen Indiana University, Jeremy G. Siek Indiana University, USA
DOI
17:00
20m
Talk
Foundational Integration Verification of a Cryptographic Server
PLDI Research Papers
Andres Erbsen Google, Jade Philipoom Google, Germany, Dustin Jamner MIT CSAIL, Ashley Lin Massachusetts Institute of Technology, Samuel Gruetter Massachusetts Institute of Technology, Clément Pit-Claudel EPFL, Adam Chlipala Massachusetts Institute of Technology
DOI
16:00 - 17:20
16:00
20m
Talk
Refined Input, Degraded Output: The Counterintuitive World of Compiler Behavior
PLDI Research Papers
Theodoros Theodoridis ETH Zurich, Zhendong Su ETH Zurich
DOI
16:20
20m
Talk
Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding
PLDI Research Papers
Qiuping Yi Texas A&M University, Yifan Yu Beijing University of Posts and Telecommunications, Guowei Yang University of Queensland
DOI
16:40
20m
Talk
Diffy: Data-Driven Bug Finding for Configurations
PLDI Research Papers
Siva Kesava Reddy Kakarla Microsoft Research, Francis Y. Yan Microsoft Research, Ryan Beckett Microsoft Research, USA
DOI
17:00
20m
Talk
Boosting Compiler Testing by Injecting Real-World Code
PLDI Research Papers
Shaohua Li ETH Zurich, Theodoros Theodoridis ETH Zurich, Zhendong Su ETH Zurich
DOI
16:00 - 17:20
Fast Linear AlgebraPLDI Research Papers at Sweden
16:00
20m
Talk
A Verified Compiler for a Functional Tensor Language
PLDI Research Papers
Amanda Liu Massachusetts Institute of Technology, Gilbert Bernstein University of Washington, Seattle, Adam Chlipala Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology
DOI
16:20
20m
Talk
[TOPLAS] (De/Re)-Composition of Data-Parallel Computations via Multi-Dimensional Homomorphism
PLDI Research Papers

DOI
16:40
20m
Talk
Compilation of Modular and General Sparse Workspaces
PLDI Research Papers
Genghan Zhang Stanford University, Olivia Hsu Stanford University, Fredrik Kjolstad Stanford University
DOI
17:00
20m
Talk
Descend: A Safe GPU Systems Programming Language
PLDI Research Papers
Bastian Köpcke University of Münster, Sergei Gorlatch University of Muenster, Michel Steuwer Technische Universität Berlin
DOI Pre-print

Thu 27 Jun

Displayed time zone: Windhoek change

09:00 - 10:10
09:00 - 10:10
10:40 - 12:20
10:40
20m
Talk
The Functional Essence of Imperative Binary Search Trees
PLDI Research Papers
Anton Lorenzen University of Edinburgh, Daan Leijen Microsoft Research, Wouter Swierstra Utrecht University, Netherlands, Sam Lindley University of Edinburgh
DOI
11:00
20m
Talk
Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq
PLDI Research Papers
Simon Spies MPI-SWS, Lennard Gäher MPI-SWS, Michael Sammler MPI-SWS, Derek Dreyer MPI-SWS
DOI
11:20
20m
Talk
Maximum Consensus Floating Point Solutions for Infeasible Low-Dimensional Linear Programs with Convex Hull as the Intermediate Representation
PLDI Research Papers
Mridul Aanjaneya Rutgers University, Santosh Nagarakatte Rutgers University
DOI
11:40
20m
Talk
Live Verification in an Interactive Proof Assistant
PLDI Research Papers
Samuel Gruetter Massachusetts Institute of Technology, Viktor Fukala Massachusetts Institute of Technology, Adam Chlipala Massachusetts Institute of Technology
DOI
12:00
20m
Talk
Predictable Verification using Intrinsic Definitions
PLDI Research Papers
Adithya Murali University of Illinois at Urbana-Champaign, Cody Rivera University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign
DOI
10:40 - 12:20
10:40
20m
Talk
Linear Matching of JavaScript Regular Expressions
PLDI Research Papers
DOI Pre-print
11:00
20m
Talk
RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
PLDI Research Papers
Michael Fitzgibbons Northeastern University, Zoe Paraskevopoulou Ethereum Foundation, Noble Mushtak Northeastern University, Michelle Thalakottur Northeastern University, Jose Sulaiman Manzur Northeastern University, Amal Ahmed Northeastern University, USA
DOI
11:20
20m
Talk
Bringing the WebAssembly Standard up to Speed with SpecTec
PLDI Research Papers
Dongjun Youn KAIST, Shin Wonho KAIST, Jaehyun Lee KAIST, Sukyoung Ryu KAIST, Joachim Breitner unaffiliated, Philippa Gardner Imperial College London, Sam Lindley University of Edinburgh, Matija Pretnar University of Ljubljana, Xiaojia Rao Imperial College, Conrad Watt Nanyang Technological University, Andreas Rossberg Independent
DOI
11:40
20m
Talk
Optimistic Stack Allocation and Dynamic Heapification for Managed Runtimes
PLDI Research Papers
Aditya Anand Indian Institute of Technology Bombay, Solai Adithya IIT Mandi, Swapnil Rustagi IIT Mandi, Priyam Seth IIT Mandi, Vijay Sundaresan IBM Canada, Daryl Maier IBM Canada, V Krishna Nandivada IIT Madras, Manas Thakur Indian Institute of Technology Bombay
DOI Pre-print
12:00
20m
Talk
Concurrent Immediate Reference Counting
PLDI Research Papers
Jaehwang Jung KAIST, Jeonghyeon Kim KAIST, Matthew J. Parkinson Microsoft Azure Research, Jeehoon Kang KAIST
DOI
10:40 - 12:20
Grammars and Code and FormalismsPLDI Research Papers at Sweden
10:40
20m
Talk
Equivalence by Canonicalization for Synthesis-Backed Refactoring
PLDI Research Papers
Justin Lubin University of California at Berkeley, Jeremy Ferguson University of California-Berkeley, Kevin Ye University of California at Berkeley, Jacob Yim UC Berkeley, Sarah E. Chasins University of California at Berkeley
DOI Pre-print
11:00
20m
Talk
PL4XGL: A Programming Language Approach to Explainable Graph Learning
PLDI Research Papers
Minseok Jeon Korea University, Jihyeok Park Korea University, Hakjoo Oh Korea University
DOI
11:20
20m
Talk
Syntactic Code Search with Sequence-to-Tree Matching
PLDI Research Papers
Gabriel Matute UC Berkeley, Wode Ni Columbia University, Titus Barik Apple, Alvin Cheung University of California at Berkeley, Sarah E. Chasins University of California at Berkeley
DOI
11:40
20m
Talk
V-Star: Learning Visibly Pushdown Grammars from Program Inputs
PLDI Research Papers
Xiaodong Jia Pennsylvania State University, Gang Tan Pennsylvania State University
DOI
12:00
20m
Talk
Hashing Modulo Context-Sensitive Alpha-Equivalence
PLDI Research Papers
Lasse Blaauwbroek Czech Institute for Informatics Robotics and Cybernetics, Miroslav Olšák Institut des Hautes Études Scientifiques, Herman Geuvers Radboud University Nijmegen, Netherlands
DOI
12:20 - 13:40
13:40 - 14:40
Formal Verification 2PLDI Research Papers at Finland / Norway
13:40
20m
Talk
Mechanised Hypersafety Proofs about Structured Data
PLDI Research Papers
Vladimir Gladshtein National University of Singapore, Qiyuan Zhao National University of Singapore, Willow Ahrens Massachusetts Institute of Technology, Saman Amarasinghe Massachusetts Institute of Technology, Ilya Sergey National University of Singapore
DOI Pre-print
14:00
20m
Talk
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties
PLDI Research Papers
Thibault Dardinier ETH Zurich, Peter Müller ETH Zurich
DOI
14:20
20m
Talk
A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata
PLDI Research Papers
Zhe Zhou Purdue University, Qianchuan Ye Purdue University, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University
DOI
13:40 - 14:40
13:40
15m
Talk
[PLDI 2023] CQS: A Formally-Verified Framework for Fair and Abortable Synchronization
PLDI Research Papers
Nikita Koval JetBrains, Dmitry Khalanskiy JetBrains, Dan Alistarh IST Austria
DOI
13:55
15m
Talk
[PLDI 2023] Program Reconditioning: Avoiding Undefined Behaviour When Finding and Reducing Compiler Bugs
PLDI Research Papers
Bastien Lecoeur Imperial College London, Hasan Mohsin Imperial College London, Alastair F. Donaldson Imperial College London
DOI
14:10
15m
Talk
[OOPSLA'23] Two Birds with One Stone: Boosting Code Generation and Code Search via a Generative Adversarial Network
PLDI Research Papers
Shangwen Wang National University of Defense Technology, Bo Lin , Zhensu Sun Singapore Management University, Ming Wen Huazhong University of Science and Technology, Yepang Liu Southern University of Science and Technology, Yan Lei Chongqing University, Xiaoguang Mao National University of Defense Technology
DOI
14:25
15m
Talk
[TOPLAS] CFLOBDDs: Context-Free-Language Ordered Binary Decision Diagrams
PLDI Research Papers

13:40 - 14:40
Solvers for Fun and ProfitPLDI Research Papers at Sweden
13:40
20m
Talk
SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques
PLDI Research Papers
Elvira Albert Complutense University of Madrid, Maria Garcia de la Banda Monash University, Alejandro Hernández-Cerezo Complutense University of Madrid, Alexey Ignatiev Monash University, Albert Rubio Complutense University of Madrid, Peter J. Stuckey Monash University
DOI
14:00
20m
Talk
Inductive Approach to Spacer
PLDI Research Papers
Takeshi Tsukada Chiba University, Hiroshi Unno Tohoku University
DOI
14:20
20m
Talk
SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories
PLDI Research Papers
Benjamin Mikek Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology
DOI

Fri 28 Jun

Displayed time zone: Windhoek change

09:00 - 10:10
09:00 - 10:10
10:40 - 12:20
10:40
20m
Talk
From Batch to Stream: Automatic Generation of Online Algorithms
PLDI Research Papers
Ziteng Wang University of Texas at Austin, Shankara Pailoor University of Texas at Austin, Aaryan Prakash University of Texas at Austin, Yuepeng Wang Simon Fraser University, Işıl Dillig University of Texas at Austin
DOI
11:00
20m
Talk
Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis
PLDI Research Papers
Ruyi Ji Peking University, Yuwei Zhao Peking University, Nadia Polikarpova University of California at San Diego, Yingfei Xiong Peking University, Zhenjiang Hu Peking University
DOI
11:20
20m
Talk
Recursive Program Synthesis using Paramorphisms
PLDI Research Papers
Qiantan Hong Stanford University, Alex Aiken Stanford University
DOI
11:40
20m
Talk
Reward-Guided Synthesis of Intelligent Agents with Control Structures
PLDI Research Papers
Guofeng Cui Rutgers University, Yuning Wang Rutgers University, Wenjie Qiu Rutgers University, He Zhu Rutgers University, USA
DOI
12:00
20m
Talk
[TOPLAS] Decomposition-Based Synthesis for Applying D&C-Like Algorithmic Paradigms
PLDI Research Papers

10:40 - 12:20
Concurrent and DistributedPLDI Research Papers at Iceland / Denmark
10:40
20m
Talk
[TOPLAS] Choral: Object-Oriented Choreographic Programming
PLDI Research Papers

11:00
20m
Talk
SPORE: Combining Symmetry and Partial Order Reduction
PLDI Research Papers
DOI
11:20
20m
Talk
IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications
PLDI Research Papers
Chujun Geng The Ohio State University, USA, Spyros Blanas Ohio State University, Michael D. Bond Ohio State University, USA, Yang Wang The Ohio State University
DOI
11:40
20m
Talk
LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
PLDI Research Papers
Longfei Qiu Yale University, Yoonseung Kim Yale University, Ji-Yong Shin Northeastern University, Jieung Kim Inha University, Wolf Honore Yale University, Zhong Shao Yale University
DOI
12:00
20m
Talk
A Family of Fast and Memory Efficient Lock- and Wait-Free Reclamation
PLDI Research Papers
Ruslan Nikolaev The Pennsylvania State University, Binoy Ravindran Virginia Tech
DOI
10:40 - 12:20
Program Analysis 1PLDI Research Papers at Sweden
10:40
20m
Talk
[TOPLAS] Interactive Abstract Interpretation with Demanded Summarization
PLDI Research Papers

11:00
20m
Talk
Efficient Static Vulnerability Analysis for JavaScript with Multiversion Dependency Graphs
PLDI Research Papers
Mafalda Ferreira INESC-ID and Universidade de Lisboa, Miguel Monteiro INESC-ID and Universidade de Lisboa, Tiago Brito INESC-ID and Universidade de Lisboa, Miguel E. Coimbra INESC-ID and Universidade de Lisboa, Nuno Santos INESC-ID / Instituto Superior Tecnico, University of Lisbon, Limin Jia , José Fragoso Santos INESC-ID/Instituto Superior Técnico, Portugal
DOI Pre-print
11:20
20m
Talk
Floating-Point TVPI Abstract Domain
PLDI Research Papers
Joao Rivera ETH Zurich, Franz Franchetti Carnegie Mellon University, USA, Markus Püschel ETH Zurich
DOI
11:40
20m
Talk
Reducing Static Analysis Unsoundness with Approximate Interpretation
PLDI Research Papers
Mathias Rud Laursen Aarhus University, Wenyuan Xu Aarhus University, Anders Møller Aarhus University
DOI
12:00
20m
Talk
Falcon: A Scalable Analytical Cache Model
PLDI Research Papers
Arjun Pitchanathan University of Edinburgh, Kunwar Grover AMD, Tobias Grosser University of Cambridge, UK
DOI
12:20 - 13:40
13:40 - 15:20
13:40
20m
Talk
Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis
PLDI Research Papers
Peisen Yao Zhejing University, Jinguo Zhou Ant Group, Xiao Xiao Ant Group, Qingkai Shi Nanjing University, Rongxin Wu School of Informatics, Xiamen University, Charles Zhang The Hong Kong University of Science and Technology
DOI
14:00
20m
Talk
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic
PLDI Research Papers
Sunho Park KAIST, Jaewoo Kim KAIST, Ike Mulder Radboud University Nijmegen, Jaehwang Jung KAIST, Janggun Lee KAIST, Robbert Krebbers Radboud University Nijmegen, Jeehoon Kang KAIST
DOI
14:20
20m
Talk
Compositional Semantics for Shared-Variable Concurrency
PLDI Research Papers
Mikhail Svyatlovskiy Tel Aviv University, Shai Mermelstein Tel Aviv University, Ori Lahav Tel Aviv University
DOI
14:40
20m
Talk
Input-Relational Verification of Deep Neural Networks
PLDI Research Papers
Debangshu Banerjee University of Illinois at Urbana-Champaign, Changming Xu University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research
DOI
15:00
20m
Talk
Automated Verification of Fundamental Algebraic Laws
PLDI Research Papers
George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen
DOI
13:40 - 15:20
Close to the HardwarePLDI Research Papers at Iceland / Denmark
13:40
20m
Talk
Allo: A Programming Model for Composable Accelerator Design
PLDI Research Papers
Hongzheng Chen Cornell University, Niansong Zhang Cornell University, Shaojie Xiang Cornell University, Zhichen Zeng University of Science and Technology of China, Mengjia Dai University of Science and Technology of China, Zhiru Zhang Cornell University, USA
DOI
14:00
20m
Talk
VESTA: Power Modeling with Language Runtime Events
PLDI Research Papers
Joseph Raskind SUNY Binghamton, Timur Babakol SUNY Binghamton, USA, Khaled Mahmoud SUNY Binghamton, USA, Yu David Liu SUNY Binghamton
DOI
14:20
20m
Talk
Modular Hardware Design of Pipelined Circuits with Hazards
PLDI Research Papers
DOI
14:40
20m
Talk
Jacdac: Service-Based Prototyping of Embedded Systems
PLDI Research Papers
Thomas Ball Microsoft Research, Peli de Halleux Microsoft Research, James Devine Microsoft, Steve Hodges Lancaster University, Michał Moskal Microsoft Research
DOI Pre-print
15:00
20m
Talk
Wavefront Threading Enables Effective High-Level Synthesis
PLDI Research Papers
Blake Pelton Microsoft, Adam Sapek Microsoft, Ken Eguro Microsoft, Daniel Lo Microsoft, Alessandro Forin Microsoft, Matt Humphrey Microsoft, Jinwen Xi Microsoft, David Cox Microsoft, Rajas Karandikar Microsoft, Johannes de Fine Licht NextSilicon, Evgeny Babin Microsoft, Adrian Caulfield Microsoft, Doug Burger Microsoft
DOI
13:40 - 15:20
Program Analysis 2PLDI Research Papers at Sweden
13:40
20m
Talk
Scaling Type-Based Points-to Analysis with Saturation
PLDI Research Papers
Christian Wimmer Oracle Labs, Codrut Stancu Oracle Labs, David Kozak Brno University of Technology & Oracle Labs, Thomas Wuerthinger Oracle Labs
DOI Pre-print
14:00
20m
Talk
Program Analysis for Adaptive Data Analysis
PLDI Research Papers
Jiawen Liu , Weihao Qu Monmouth University, Marco Gaboardi Boston University, Deepak Garg MPI-SWS, Jonathan Ullman Northeastern University
DOI
14:20
20m
Talk
Robust Resource Bounds with Static Analysis and Bayesian Inference
PLDI Research Papers
Long Pham Carnegie Mellon University, Feras Saad Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University
DOI
14:40
20m
Talk
Context-Free Language Reachability via Skewed Tabulation
PLDI Research Papers
Yuxiang Lei UNSW Sydney, Camille Bossut Georgia Institute of Technology, Yulei Sui UNSW Sydney, Qirun Zhang Georgia Institute of Technology
DOI
15:00
20m
Talk
Static Analysis for Checking the Disambiguation Robustness of Regular Expressions
PLDI Research Papers
Konstantinos Mamouras Rice University, Alexis Le Glaunec Rice University, Wu Angela Li Rice University, Agnishom Chattopadhyay Rice University
DOI

Accepted Papers

Title
A Family of Fast and Memory Efficient Lock- and Wait-Free Reclamation
PLDI Research Papers
DOI
A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata
PLDI Research Papers
DOI
A Lightweight Polyglot Code Transformation Language
PLDI Research Papers
DOI Pre-print
Allo: A Programming Model for Composable Accelerator Design
PLDI Research Papers
DOI
An Algebraic Language for Specifying Quantum Networks
PLDI Research Papers
DOI
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic
PLDI Research Papers
DOI
Associated Effects
PLDI Research Papers
DOI
A Tensor Compiler with Automatic Data Packing for Simple and Efficient Fully Homomorphic Encryption
PLDI Research Papers
DOI
Automated Verification of Fundamental Algebraic Laws
PLDI Research Papers
DOI
A Verified Compiler for a Functional Tensor Language
PLDI Research Papers
DOI
Bit Blasting Probabilistic Programs
PLDI Research Papers
DOI
Boosting Compiler Testing by Injecting Real-World Code
PLDI Research Papers
DOI
Bringing the WebAssembly Standard up to Speed with SpecTec
PLDI Research Papers
DOI
Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding
PLDI Research Papers
DOI
Compilation of Modular and General Sparse Workspaces
PLDI Research Papers
DOI
Compilation of Qubit Circuits to Optimized Qutrit Circuits
PLDI Research Papers
DOI
Compiling Conditional Quantum Gates without Using Helper Qubits
PLDI Research Papers
DOI
Compiling Probabilistic Programs for Variable Elimination with Information Flow
PLDI Research Papers
DOI
Compiling with Abstract Interpretation
PLDI Research Papers
DOI
Compositional Semantics for Shared-Variable Concurrency
PLDI Research Papers
DOI
Concurrent Immediate Reference Counting
PLDI Research Papers
DOI
Consolidating Smart Contracts with Behavioral Contracts
PLDI Research Papers
DOI
Context-Free Language Reachability via Skewed Tabulation
PLDI Research Papers
DOI
Daedalus: Safer Document Parsing
PLDI Research Papers
DOI
Decidable Subtyping of Existential Types for Julia
PLDI Research Papers
DOI
Descend: A Safe GPU Systems Programming Language
PLDI Research Papers
DOI Pre-print
Diffy: Data-Driven Bug Finding for Configurations
PLDI Research Papers
DOI
Don’t Write, but Return: Replacing Output Parameters with Algebraic Data Types in C-to-Rust Translation
PLDI Research Papers
DOI
Efficient Static Vulnerability Analysis for JavaScript with Multiversion Dependency Graphs
PLDI Research Papers
DOI Pre-print
Equivalence and Similarity Refutation for Probabilistic Programs
PLDI Research Papers
DOI
Equivalence by Canonicalization for Synthesis-Backed Refactoring
PLDI Research Papers
DOI Pre-print
Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis
PLDI Research Papers
DOI
Falcon: A Scalable Analytical Cache Model
PLDI Research Papers
DOI
Floating-Point TVPI Abstract Domain
PLDI Research Papers
DOI
Foundational Integration Verification of a Cryptographic Server
PLDI Research Papers
DOI
From Batch to Stream: Automatic Generation of Online Algorithms
PLDI Research Papers
DOI
GenSQL: A Probabilistic Programming System for Querying Generative Models of Database Tables
PLDI Research Papers
DOI
Hashing Modulo Context-Sensitive Alpha-Equivalence
PLDI Research Papers
DOI
Hyperblock Scheduling for Verified High-Level Synthesis
PLDI Research Papers
DOI Pre-print
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties
PLDI Research Papers
DOI
Inductive Approach to Spacer
PLDI Research Papers
DOI
Input-Relational Verification of Deep Neural Networks
PLDI Research Papers
DOI
IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications
PLDI Research Papers
DOI
Jacdac: Service-Based Prototyping of Embedded Systems
PLDI Research Papers
DOI Pre-print
KATch: A Fast Symbolic Verifier for NetKAT
PLDI Research Papers
DOI
LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
PLDI Research Papers
DOI
Linear Matching of JavaScript Regular Expressions
PLDI Research Papers
DOI Pre-print
Live Verification in an Interactive Proof Assistant
PLDI Research Papers
DOI
Maximum Consensus Floating Point Solutions for Infeasible Low-Dimensional Linear Programs with Convex Hull as the Intermediate Representation
PLDI Research Papers
DOI
Mechanised Hypersafety Proofs about Structured Data
PLDI Research Papers
DOI Pre-print
Modular Hardware Design of Pipelined Circuits with Hazards
PLDI Research Papers
DOI
NetBlocks: Staging Layouts for High-Performance Custom Host Network Stacks
PLDI Research Papers
DOI
Numerical Fuzz: A Type System for Rounding Error Analysis
PLDI Research Papers
DOI
Optimistic Stack Allocation and Dynamic Heapification for Managed Runtimes
PLDI Research Papers
DOI Pre-print
PL4XGL: A Programming Language Approach to Explainable Graph Learning
PLDI Research Papers
DOI
[PLDI 2023] CQS: A Formally-Verified Framework for Fair and Abortable Synchronization
PLDI Research Papers
DOI
Predictable Verification using Intrinsic Definitions
PLDI Research Papers
DOI
Probabilistic Programming with Programmable Variational Inference
PLDI Research Papers
DOI
Program Analysis for Adaptive Data Analysis
PLDI Research Papers
DOI
Quantitative Robustness for Vulnerability Assessment
PLDI Research Papers
DOI
Qubit Recycling Revisited
PLDI Research Papers
DOI
Quest Complete: The Holy Grail of Gradual Security
PLDI Research Papers
DOI
Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq
PLDI Research Papers
DOI
Recursive Program Synthesis using Paramorphisms
PLDI Research Papers
DOI
Reducing Static Analysis Unsoundness with Approximate Interpretation
PLDI Research Papers
DOI
Refined Input, Degraded Output: The Counterintuitive World of Compiler Behavior
PLDI Research Papers
DOI
RefinedRust: A Type System for High-Assurance Verification of Rust Programs
PLDI Research Papers
DOI
Reward-Guided Synthesis of Intelligent Agents with Control Structures
PLDI Research Papers
DOI
RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
PLDI Research Papers
DOI
Robust Resource Bounds with Static Analysis and Bayesian Inference
PLDI Research Papers
DOI
Scaling Type-Based Points-to Analysis with Saturation
PLDI Research Papers
DOI Pre-print
SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories
PLDI Research Papers
DOI
Space-Efficient Polymorphic Gradual Typing, Mostly Parametric
PLDI Research Papers
DOI
SpEQ: Translation of Sparse Codes using Equivalences
PLDI Research Papers
DOI Pre-print
SPORE: Combining Symmetry and Partial Order Reduction
PLDI Research Papers
DOI
Static Analysis for Checking the Disambiguation Robustness of Regular Expressions
PLDI Research Papers
DOI
Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
PLDI Research Papers
DOI
Stream Types
PLDI Research Papers
DOI
Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis
PLDI Research Papers
DOI
SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques
PLDI Research Papers
DOI
Symbolic Execution for Quantum Error Correction Programs
PLDI Research Papers
DOI
Syntactic Code Search with Sequence-to-Tree Matching
PLDI Research Papers
DOI
The Functional Essence of Imperative Binary Search Trees
PLDI Research Papers
DOI
The T-Complexity Costs of Error Correction for Control Flow in Quantum Computation
PLDI Research Papers
DOI
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language
PLDI Research Papers
DOI
Verification under Intel-x86 with Persistency
PLDI Research Papers
DOI
Verified Extraction from Coq to OCaml
PLDI Research Papers
DOI
VESTA: Power Modeling with Language Runtime Events
PLDI Research Papers
DOI
V-Star: Learning Visibly Pushdown Grammars from Program Inputs
PLDI Research Papers
DOI
Wavefront Threading Enables Effective High-Level Synthesis
PLDI Research Papers
DOI

Call for Papers


Please note that the “Artifact Evaluation for Accepted Papers” section has been modified a bit from previous years’.


PACMPL Issue PLDI 2024 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 2024 will be invited – but not required – to present their work in the PLDI conference in June 2024, which is sponsored by ACM SIGPLAN.

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.

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 assesses 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, with extremely rare extenuating circumstances considered at the discretion of the Associate Editor.

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://pldi2024.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 16, 2023 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 submmitted using numeric citations, but final versions of accepted papers must use author-year 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.

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 for Accepted Papers

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 and 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.

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.

These choices follow from ACM Copyright Policy and ACM Author Rights, corresponding to ACM’s “author pays” option. While PACMPL may ask authors who have funding for open-access fees to voluntarily cover the article processing charge (currently, US$400), payment is not required for publication. PACMPL and SIGPLAN continue to explore the best models for funding open access, focusing on approaches that are sustainable in the long-term while reducing short-term risk.

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.

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.