PLDI 2021
42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021)

Title Page

Article: pldi21foreword-fm000-p (type: Frontmatter) doi:

Welcome from the Chairs

Article: pldi21foreword-fm001-p (type: Frontmatter) doi:

PLDI 2021 Organization

Article: pldi21foreword-fm002-p (type: Frontmatter) doi:

Sponsors

Article: pldi21foreword-fm003-p (type: Frontmatter) doi:

Incremental Whole-Program Analysis in Datalog with Lattices
Tamás Szabó, Sebastian Erdweg, and Gábor Bergmann
(JGU Mainz, Germany; Workday, Germany; Budapest University of Technology and Economics, Hungary; IncQuery Labs, Hungary)

@InProceedings{PLDI21p1, author = {Tamás Szabó and Sebastian Erdweg and Gábor Bergmann}, title = {Incremental Whole-Program Analysis in Datalog with Lattices}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1-0}, doi = {10.1145/3453483.3454026}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p12-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454026

Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8
Kyeongmin Cho, Sung-Hwan Lee, Azalea Raad, and Jeehoon Kang
(KAIST, South Korea; Seoul National University, South Korea; Imperial College London, UK)

@InProceedings{PLDI21p19, author = {Kyeongmin Cho and Sung-Hwan Lee and Azalea Raad and Jeehoon Kang}, title = {Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {19-18}, doi = {10.1145/3453483.3454027}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p21-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454027

Repairing Serializability Bugs in Distributed Database Programs via Automated Schema Refactoring
Kia Rahmani, Kartik Nagar, Benjamin Delaware, and Suresh Jagannathan
(Purdue University, USA; IIT Madras, India)

@InProceedings{PLDI21p37, author = {Kia Rahmani and Kartik Nagar and Benjamin Delaware and Suresh Jagannathan}, title = {Repairing Serializability Bugs in Distributed Database Programs via Automated Schema Refactoring}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {37-36}, doi = {10.1145/3453483.3454028}, year = {2021}, } Publisher's Version Article: pldi21main-p25-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454028

Gleipnir: Toward Practical Error Analysis for Quantum Programs
Runzhou Tao, Yunong Shi, Jianan Yao, John Hui, Frederic T. Chong, and Ronghui Gu
(Columbia University, USA; University of Chicago, USA)

@InProceedings{PLDI21p55, author = {Runzhou Tao and Yunong Shi and Jianan Yao and John Hui and Frederic T. Chong and Ronghui Gu}, title = {Gleipnir: Toward Practical Error Analysis for Quantum Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {55-54}, doi = {10.1145/3453483.3454029}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi21main-p27-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454029

Alive2: Bounded Translation Validation for LLVM
Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr
(Microsoft Research, UK; Seoul National University, South Korea; University of Utah, USA)

@InProceedings{PLDI21p73, author = {Nuno P. Lopes and Juneyoung Lee and Chung-Kil Hur and Zhengyang Liu and John Regehr}, title = {Alive2: Bounded Translation Validation for LLVM}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {73-72}, doi = {10.1145/3453483.3454030}, year = {2021}, } Publisher's Version Article: pldi21main-p30-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454030

Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic
Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, and Lars Birkedal
(MPI-SWS, Germany; Saarland University, Germany; Aarhus University, Denmark; Boston College, USA; Radboud University Nijmegen, Netherlands)

@InProceedings{PLDI21p91, author = {Simon Spies and Lennard Gäher and Daniel Gratzer and Joseph Tassarotti and Robbert Krebbers and Derek Dreyer and Lars Birkedal}, title = {Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {91-90}, doi = {10.1145/3453483.3454031}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p34-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454031

Perceus: Garbage Free Reference Counting with Reuse
Alex Reinking, Ningning Xie, Leonardo de Moura, and Daan Leijen
(Microsoft Research, USA; University of Hong Kong, China)

@InProceedings{PLDI21p109, author = {Alex Reinking and Ningning Xie and Leonardo de Moura and Daan Leijen}, title = {Perceus: Garbage Free Reference Counting with Reuse}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {109-108}, doi = {10.1145/3453483.3454032}, year = {2021}, } Publisher's Version Article: pldi21main-p40-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454032

Proof Repair across Type Equivalences
Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, and Dan Grossman
(University of Washington, USA; Northeastern University, USA; Halfaya Research, USA)

@InProceedings{PLDI21p127, author = {Talia Ringer and RanDair Porter and Nathaniel Yazdani and John Leo and Dan Grossman}, title = {Proof Repair across Type Equivalences}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {127-126}, doi = {10.1145/3453483.3454033}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p43-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454033

Compiler-Assisted Object Inlining with Value Fields
Rodrigo Bruno, Vojin Jovanovic, Christian Wimmer, and Gustavo Alonso
(Oracle Labs, Switzerland; Oracle Labs, USA; ETH Zurich, Switzerland)

@InProceedings{PLDI21p145, author = {Rodrigo Bruno and Vojin Jovanovic and Christian Wimmer and Gustavo Alonso}, title = {Compiler-Assisted Object Inlining with Value Fields}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {145-144}, doi = {10.1145/3453483.3454034}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p44-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454034

Unleashing the Hidden Power of Compiler Optimization on Binary Code Difference: An Empirical Study
Xiaolei Ren, Michael Ho, Jiang Ming, Yu Lei, and Li Li
(University of Texas at Arlington, USA; Monash University, Australia)

@InProceedings{PLDI21p163, author = {Xiaolei Ren and Michael Ho and Jiang Ming and Yu Lei and Li Li}, title = {Unleashing the Hidden Power of Compiler Optimization on Binary Code Difference: An Empirical Study}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {163-162}, doi = {10.1145/3453483.3454035}, year = {2021}, } Publisher's Version Article: pldi21main-p45-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454035

RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types
Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg
(MPI-SWS, Germany; Radboud University Nijmegen, Netherlands; University of Cambridge, UK)

@InProceedings{PLDI21p181, author = {Michael Sammler and Rodolphe Lepigre and Robbert Krebbers and Kayvan Memarian and Derek Dreyer and Deepak Garg}, title = {RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {181-180}, doi = {10.1145/3453483.3454036}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p67-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454036

Wire Sorts: A Language Abstraction for Safe Hardware Composition
Michael Christensen, Timothy Sherwood, Jonathan Balkind, and Ben Hardekopf
(University of California at Santa Barbara, USA)

@InProceedings{PLDI21p199, author = {Michael Christensen and Timothy Sherwood and Jonathan Balkind and Ben Hardekopf}, title = {Wire Sorts: A Language Abstraction for Safe Hardware Composition}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {199-198}, doi = {10.1145/3453483.3454037}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p72-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454037

DeepCuts: A Deep Learning Optimization Framework for Versatile GPU Workloads
Wookeun Jung, Thanh Tuan Dao, and Jaejin Lee
(Seoul National University, South Korea)

@InProceedings{PLDI21p217, author = {Wookeun Jung and Thanh Tuan Dao and Jaejin Lee}, title = {DeepCuts: A Deep Learning Optimization Framework for Versatile GPU Workloads}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {217-216}, doi = {10.1145/3453483.3454038}, year = {2021}, } Publisher's Version Article: pldi21main-p76-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454038

Retrofitting Effect Handlers onto OCaml
KC Sivaramakrishnan, Stephen Dolan, Leo White, Tom Kelly, Sadiq Jaffer, and Anil Madhavapeddy
(IIT Madras, India; OCaml Labs, UK; Jane Street, UK; Opsian, UK; University of Cambridge, UK)

@InProceedings{PLDI21p235, author = {KC Sivaramakrishnan and Stephen Dolan and Leo White and Tom Kelly and Sadiq Jaffer and Anil Madhavapeddy}, title = {Retrofitting Effect Handlers onto OCaml}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {235-234}, doi = {10.1145/3453483.3454039}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi21main-p82-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454039

Unqomp: Synthesizing Uncomputation in Quantum Circuits
Anouk Paradis, Benjamin Bichsel, Samuel Steffen, and Martin Vechev
(ETH Zurich, Switzerland)

@InProceedings{PLDI21p253, author = {Anouk Paradis and Benjamin Bichsel and Samuel Steffen and Martin Vechev}, title = {Unqomp: Synthesizing Uncomputation in Quantum Circuits}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {253-252}, doi = {10.1145/3453483.3454040}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p83-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454040

Zooid: A DSL for Certified Multiparty Computation: From Mechanised Metatheory to Certified Multiparty Processes
David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, and Nobuko Yoshida
(Imperial College London, UK; University of Kent, UK)

@InProceedings{PLDI21p271, author = {David Castro-Perez and Francisco Ferreira and Lorenzo Gheri and Nobuko Yoshida}, title = {Zooid: A DSL for Certified Multiparty Computation: From Mechanised Metatheory to Certified Multiparty Processes}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {271-270}, doi = {10.1145/3453483.3454041}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p92-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454041

Fluid: A Framework for Approximate Concurrency via Controlled Dependency Relaxation
Huaipan Jiang, Haibo Zhang, Xulong Tang, Vineetha Govindaraj, Jack Sampson, Mahmut Taylan Kandemir, and Danfeng Zhang
(Pennsylvania State University, USA; University of Pittsburgh, USA)

@InProceedings{PLDI21p289, author = {Huaipan Jiang and Haibo Zhang and Xulong Tang and Vineetha Govindaraj and Jack Sampson and Mahmut Taylan Kandemir and Danfeng Zhang}, title = {Fluid: A Framework for Approximate Concurrency via Controlled Dependency Relaxation}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {289-288}, doi = {10.1145/3453483.3454042}, year = {2021}, } Publisher's Version Article: pldi21main-p99-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454042

Developer and User-Transparent Compiler Optimization for Interactive Applications
Paschalis Mpeis, Pavlos Petoumenos, Kim Hazelwood, and Hugh Leather
(University of Edinburgh, UK; University of Manchester, UK; Facebook, USA)

@InProceedings{PLDI21p307, author = {Paschalis Mpeis and Pavlos Petoumenos and Kim Hazelwood and Hugh Leather}, title = {Developer and User-Transparent Compiler Optimization for Interactive Applications}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {307-306}, doi = {10.1145/3453483.3454043}, year = {2021}, } Publisher's Version Article: pldi21main-p106-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454043

Demanded Abstract Interpretation
Benno Stein, Bor-Yuh Evan Chang, and Manu Sridharan
(University of Colorado at Boulder, USA; Amazon, USA; University of California at Riverside, USA)

@InProceedings{PLDI21p325, author = {Benno Stein and Bor-Yuh Evan Chang and Manu Sridharan}, title = {Demanded Abstract Interpretation}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {325-324}, doi = {10.1145/3453483.3454044}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p111-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454044

Learning to Find Naming Issues with Big Code and Small Supervision
Jingxuan He, Cheng-Chun Lee, Veselin Raychev, and Martin Vechev
(ETH Zurich, Switzerland; EPFL, Switzerland; Snyk, Switzerland)

@InProceedings{PLDI21p343, author = {Jingxuan He and Cheng-Chun Lee and Veselin Raychev and Martin Vechev}, title = {Learning to Find Naming Issues with Big Code and Small Supervision}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {343-342}, doi = {10.1145/3453483.3454045}, year = {2021}, } Publisher's Version Article: pldi21main-p112-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454045

DIY Assistant: A Multi-modal End-User Programmable Virtual Assistant
Michael H. Fischer, Giovanni Campagna, Euirim Choi, and Monica S. Lam
(Stanford University, USA)

@InProceedings{PLDI21p361, author = {Michael H. Fischer and Giovanni Campagna and Euirim Choi and Monica S. Lam}, title = {DIY Assistant: A Multi-modal End-User Programmable Virtual Assistant}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {361-360}, doi = {10.1145/3453483.3454046}, year = {2021}, } Publisher's Version Article: pldi21main-p115-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454046

Web Question Answering with Neurosymbolic Program Synthesis
Qiaochu Chen, Aaron Lamoreaux, Xinyu Wang, Greg Durrett, Osbert Bastani, and Isil Dillig
(University of Texas at Austin, USA; University of Michigan, USA; University of Pennsylvania, USA)

@InProceedings{PLDI21p379, author = {Qiaochu Chen and Aaron Lamoreaux and Xinyu Wang and Greg Durrett and Osbert Bastani and Isil Dillig}, title = {Web Question Answering with Neurosymbolic Program Synthesis}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {379-378}, doi = {10.1145/3453483.3454047}, year = {2021}, } Publisher's Version Article: pldi21main-p121-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454047

RbSyn: Type- and Effect-Guided Program Synthesis
Sankha Narayan Guria, Jeffrey S. Foster, and David Van Horn
(University of Maryland, USA; Tufts University, USA)

@InProceedings{PLDI21p397, author = {Sankha Narayan Guria and Jeffrey S. Foster and David Van Horn}, title = {RbSyn: Type- and Effect-Guided Program Synthesis}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {397-396}, doi = {10.1145/3453483.3454048}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p124-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454048

High Performance Correctly Rounded Math Libraries for 32-bit Floating Point Representations
Jay P. Lim and Santosh Nagarakatte
(Rutgers University, USA)

@InProceedings{PLDI21p415, author = {Jay P. Lim and Santosh Nagarakatte}, title = {High Performance Correctly Rounded Math Libraries for 32-bit Floating Point Representations}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {415-414}, doi = {10.1145/3453483.3454049}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p126-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454049

Porcupine: A Synthesizing Compiler for Vectorized Homomorphic Encryption
Meghan Cowan, Deeksha Dangwal, Armin Alaghi, Caroline Trippel, Vincent T. Lee, and Brandon Reagen
(Facebook Reality Labs Research, USA; Stanford University, USA; New York University, USA)

@InProceedings{PLDI21p433, author = {Meghan Cowan and Deeksha Dangwal and Armin Alaghi and Caroline Trippel and Vincent T. Lee and Brandon Reagen}, title = {Porcupine: A Synthesizing Compiler for Vectorized Homomorphic Encryption}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {433-432}, doi = {10.1145/3453483.3454050}, year = {2021}, } Publisher's Version Article: pldi21main-p127-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454050

Concolic Program Repair
Ridwan Shariffdeen, Yannic Noller, Lars Grunske, and Abhik Roychoudhury
(National University of Singapore, Singapore; Humboldt University of Berlin, Germany)

@InProceedings{PLDI21p451, author = {Ridwan Shariffdeen and Yannic Noller and Lars Grunske and Abhik Roychoudhury}, title = {Concolic Program Repair}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {451-450}, doi = {10.1145/3453483.3454051}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p130-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454051

Concise, Type-Safe, and Efficient Structural Diffing
Sebastian Erdweg, Tamás Szabó, and André Pacak
(JGU Mainz, Germany; Workday, Germany)

@InProceedings{PLDI21p469, author = {Sebastian Erdweg and Tamás Szabó and André Pacak}, title = {Concise, Type-Safe, and Efficient Structural Diffing}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {469-468}, doi = {10.1145/3453483.3454052}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p144-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454052

CoStar: A Verified ALL(*) Parser
Sam Lasser, Chris Casinghino, Kathleen Fisher, and Cody Roux
(Tufts University, USA; Draper, USA)

@InProceedings{PLDI21p487, author = {Sam Lasser and Chris Casinghino and Kathleen Fisher and Cody Roux}, title = {CoStar: A Verified ALL(*) Parser}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {487-486}, doi = {10.1145/3453483.3454053}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p145-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454053

Automated Conformance Testing for JavaScript Engines via Deep Compiler Fuzzing
Guixin Ye, Zhanyong Tang, Shin Hwei Tan, Songfang Huang, Dingyi Fang, Xiaoyang Sun, Lizhong Bian, Haibo Wang, and Zheng Wang
(Northwest University, China; Southern University of Science and Technology, China; Alibaba DAMO Academy, China; University of Leeds, UK; Alipay, China)

@InProceedings{PLDI21p505, author = {Guixin Ye and Zhanyong Tang and Shin Hwei Tan and Songfang Huang and Dingyi Fang and Xiaoyang Sun and Lizhong Bian and Haibo Wang and Zheng Wang}, title = {Automated Conformance Testing for JavaScript Engines via Deep Compiler Fuzzing}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {505-504}, doi = {10.1145/3453483.3454054}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi21main-p149-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454054

Beyond the Elementary Representations of Program Invariants over Algebraic Data Types
Yurii Kostyukov, Dmitry Mordvinov, and Grigory Fedyukovich
(St. Petersburg State University, Russia; JetBrains Research, Russia; Florida State University, USA)

@InProceedings{PLDI21p523, author = {Yurii Kostyukov and Dmitry Mordvinov and Grigory Fedyukovich}, title = {Beyond the Elementary Representations of Program Invariants over Algebraic Data Types}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {523-522}, doi = {10.1145/3453483.3454055}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi21main-p155-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454055

Fast and Precise Certification of Transformers
Gregory Bonaert, Dimitar I. Dimitrov, Maximilian Baader, and Martin Vechev
(ETH Zurich, Switzerland)

@InProceedings{PLDI21p541, author = {Gregory Bonaert and Dimitar I. Dimitrov and Maximilian Baader and Martin Vechev}, title = {Fast and Precise Certification of Transformers}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {541-540}, doi = {10.1145/3453483.3454056}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi21main-p156-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454056

Trace-Based Control-Flow Analysis
Benoît Montagu and Thomas Jensen
(Inria, France)

@InProceedings{PLDI21p559, author = {Benoît Montagu and Thomas Jensen}, title = {Trace-Based Control-Flow Analysis}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {559-558}, doi = {10.1145/3453483.3454057}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p165-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454057

Compiling Stan to Generative Probabilistic Languages and Extension to Deep Probabilistic Programming
Guillaume Baudart, Javier Burroni, Martin Hirzel, Louis Mandel, and Avraham Shinnar
(Inria, France; PSL University, France; University of Massachusetts at Amherst, USA; IBM Research, USA)

@InProceedings{PLDI21p577, author = {Guillaume Baudart and Javier Burroni and Martin Hirzel and Louis Mandel and Avraham Shinnar}, title = {Compiling Stan to Generative Probabilistic Languages and Extension to Deep Probabilistic Programming}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {577-576}, doi = {10.1145/3453483.3454058}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p166-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454058

Filling Typed Holes with Live GUIs
Cyrus Omar, David Moon, Andrew Blinn, Ian Voysey, Nick Collins, and Ravi Chugh
(University of Michigan, USA; Carnegie Mellon University, USA; University of Chicago, USA)

@InProceedings{PLDI21p595, author = {Cyrus Omar and David Moon and Andrew Blinn and Ian Voysey and Nick Collins and Ravi Chugh}, title = {Filling Typed Holes with Live GUIs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {595-594}, doi = {10.1145/3453483.3454059}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p174-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454059

Concurrent Deferred Reference Counting with Constant-Time Overhead
Daniel Anderson, Guy E. Blelloch, and Yuanhao Wei
(Carnegie Mellon University, USA)

@InProceedings{PLDI21p613, author = {Daniel Anderson and Guy E. Blelloch and Yuanhao Wei}, title = {Concurrent Deferred Reference Counting with Constant-Time Overhead}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {613-612}, doi = {10.1145/3453483.3454060}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p180-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454060

Quantum Abstract Interpretation
Nengkun Yu and Jens Palsberg
(University of Technology Sydney, Australia; University of California at Los Angeles, USA)

@InProceedings{PLDI21p631, author = {Nengkun Yu and Jens Palsberg}, title = {Quantum Abstract Interpretation}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {631-630}, doi = {10.1145/3453483.3454061}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p203-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454061

Central Moment Analysis for Cost Accumulators in Probabilistic Programs
Di Wang, Jan Hoffmann, and Thomas Reps
(Carnegie Mellon University, USA; University of Wisconsin, USA)

@InProceedings{PLDI21p649, author = {Di Wang and Jan Hoffmann and Thomas Reps}, title = {Central Moment Analysis for Cost Accumulators in Probabilistic Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {649-648}, doi = {10.1145/3453483.3454062}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p227-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454062

Synthesizing Data Structure Refinements from Integrity Constraints
Shankara Pailoor, Yuepeng Wang, Xinyu Wang, and Isil Dillig
(University of Texas at Austin, USA; University of Pennsylvania, USA; University of Michigan, USA)

@InProceedings{PLDI21p667, author = {Shankara Pailoor and Yuepeng Wang and Xinyu Wang and Isil Dillig}, title = {Synthesizing Data Structure Refinements from Integrity Constraints}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {667-666}, doi = {10.1145/3453483.3454063}, year = {2021}, } Publisher's Version Article: pldi21main-p228-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454063

Provable Repair of Deep Neural Networks
Matthew Sotoudeh and Aditya V. Thakur
(University of California at Davis, USA)

@InProceedings{PLDI21p685, author = {Matthew Sotoudeh and Aditya V. Thakur}, title = {Provable Repair of Deep Neural Networks}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {685-684}, doi = {10.1145/3453483.3454064}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional Article: pldi21main-p243-p (type: Full Paper (12 pages + 2 optional pages with charge + references)) doi:10.1145/3453483.3454064

Integration Verification across Software and Hardware for a Simple Embedded System
Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, and Adam Chlipala
(Massachusetts Institute of Technology, USA)

@InProceedings{PLDI21p703, author = {Andres Erbsen and Samuel Gruetter and Joonwon Choi and Clark Wood and Adam Chlipala}, title = {Integration Verification across Software and Hardware for a Simple Embedded System}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {703-702}, doi = {10.1145/3453483.3454065}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available<