Program - PLDI 2022

Mon 13 - Fri 17 June 2022 San Diego, California, United States

Detailed Table Column Timeline Session Timeline Detailed Timeline

Get Calendar (iCal)

Time Zone

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

Use conference time zone: (GMT-07:00) Pacific 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

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

Mon 13 Jun
Displayed time zone: Pacific Time (US & Canada) change

Mon 13 Jun

Rousseau Center

8:00

Registration

8:20

8:40

9:00

Competitive Programming with AlphaCode

Verified Trustworthy Software Specification

Philippa Gardner

Multidimensional C++

+12hMaking C Programs Safer with Checked C

Jie Zhou, Yudi Yang, Michael Hicks, John Criswell

Three years of analyzing Ada code with Infer: a retrospective

Boris Yakobowski

+12hDiscover[i]: Taming Unbounded Distributed Systems with Modular, Bounded Reasoning

Roopsha Samanta, Nouraldin Jaber, Christopher Wagner

+12hBuild your own optimizer with egg!

Max Willsey, Zachary Tatlock

9:20

9:40

10:00

10:20

+12hHigher-order function specialization in Infer

Corentin De Souza

+12hImproving Software Reliability using Machine Learning

Welcome Remarks

Azadeh Farzan, Constantin Enea, Eric Koskinen

Mentoring Panel: Surviving Grad School

Sunjay Cauligi, Ethan Cecchetti, Niki Vazou, Ningning Xie, Tamara Rezk

+12hDistributed parallel computing with Futhark

Michaël El Kharroubi, Baptiste Coudray, Orestis Malaspinas

+12hMaking C Programs Safer with Checked C

Jie Zhou, Yudi Yang, Michael Hicks, John Criswell

+12hDiscover[i]: Taming Unbounded Distributed Systems with Modular, Bounded Reasoning

Roopsha Samanta, Nouraldin Jaber, Christopher Wagner

+12hBuild your own optimizer with egg!

Max Willsey, Zachary Tatlock

10:40

Practical Smart Contract Sharding with Commutativity Analysis

+12hMech: An Array Programming Language for Robots (extended abstract)

11:00

+12hInfERL: Scalable and extensible static analysis for Erlang

+12hProductivity Assessment of Neural Code Completion

Albert Ziegler, Eirini Kalliamvakou, X. Alice Li, Andrew Rice, Devon Rifkin, Shawn Simister, Ganesh Sittampalam, Eddie Aftandilian

+12hProbabilistic Array Programming on Galois Fields (extended abstract)

Breandan Considine, Jin L.C. Guo, Xujie Si

11:20

Commutativity reasoning for automated distributed coordination

+12hPredictive Synthesis of API-Centric Code

Daye Nam, Baishakhi Ray, Seohyun Kim, xianshan qu, Satish Chandra

+12hParallel Scan As a Multidimensional Array Problem

Artjoms Šinkarovs, Sven-Bodo Scholz

11:40

+12hFrom Perception to Programs: Regularize, Overparameterize, and Amortize

Hao Tang, Kevin Ellis

12:00

12:20

12:40

13:00

13:20

+12hCan Transformers Code?

A Tree Clock Data Structure for Causal Orderings in Concurrent Executions

Andreas Pavlogiannis

+12hYour Research and Everyone Else

Martin C. Rinard

+12hCombinatory Logic and Combinators in Array Languages

+12hReasoning About and Discovering LLVM Optimizations

John Regehr, Nuno P. Lopes

+12h Finding Real Bugs in Big Programs with Incorrectness Logic

Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, Peter W. O'Hearn

+12hFilling the gap between the JavaScript language specification and tools using the JISET family

Sukyoung Ryu, Jihyeok Park, Seungmin An

13:40

+12hFrom Functional to Imperative: Combining Destination-Passing Style and Views

Zhitao Lin, Christophe Dubach

14:00

Commutativity condition synthesis and language support for commute blocks

+12hSyntax-Guided Program Reduction for Understanding Neural Code Intelligence Models

Rafiqul Rabin, Aftab Hussain, Amin Alipour

14:20

+12hHIPPODROME: Data Race Repair using Static Analysis Summaries

Andreea Costea, Abhishek Tiwari, Sigmund Chianasta, Kishore R, Abhik Roychoudhury, Ilya Sergey

+12hA Systematic Evaluation of Large Language Models of Code

Frank F. Xu, Uri Alon, Graham Neubig, Vincent J. Hellendoorn

+12hUsing Q-Learning to Select the Best Among Functionally Equivalent Implementations

Meggie van den Oever, Lauren Grimley, Richard Veras

14:40

+12hPoster Session

Lightning: Servois2: An Extended Commutativity Condition Synthesizer

15:00

15:20

+12hUnsupervised Program Synthesis: Hierarchy and Perception

Commutativity Reasoning in the Civl Verifier

+12hHow to Write a Technical Paper

+12hReasoning About and Discovering LLVM Optimizations

John Regehr, Nuno P. Lopes

+12hInfer#’s journey to bring Infer to the .NET world

Xin Shi, Xiaoyu Liu, Matthew Jin, Neel Sundaresan

+12hFilling the gap between the JavaScript language specification and tools using the JISET family

Sukyoung Ryu, Jihyeok Park, Seungmin An

15:40

16:00

Commutativity in quantum computing

+12hExeBench: An ML-scale dataset of executable C functions

Jordi Armengol-Estapé, Jackson Woodruff, Alexander Brauckmann, José Wesley de Souza Magalhães, Michael F. P. O'Boyle

16:20

+12h Infer in the cloud: An Overview of Infer Usage via Sonatype Lift

Rishav Mishra, Stephen Magill

+12hAutomatically Debugging AutoML Pipelines Using Maro: ML Automated Remediation Oracle

Julian Dolby, Jason Tsay, Martin Hirzel

16:40

+12hA Graph Neural Network-based performance model for Deep Learning Applications

Shikhar Singh, James Hegarty, Hugh Leather, Benoit Steiner

Lightning-2

17:00

17:20

17:40

18:00

18:20

18:40

19:00

19:20

19:40

20:00

20:20

20:40

21:00

Making C Programs Safer with Checked C

Jie Zhou, Yudi Yang, Michael Hicks, John Criswell

Discover[i]: Taming Unbounded Distributed Systems with Modular, Bounded Reasoning

Roopsha Samanta, Nouraldin Jaber, Christopher Wagner

Build your own optimizer with egg!

Max Willsey, Zachary Tatlock

21:20

21:40

22:00

22:20

Higher-order function specialization in Infer

Corentin De Souza

Improving Software Reliability using Machine Learning

Distributed parallel computing with Futhark

Michaël El Kharroubi, Baptiste Coudray, Orestis Malaspinas

Making C Programs Safer with Checked C

Jie Zhou, Yudi Yang, Michael Hicks, John Criswell

Discover[i]: Taming Unbounded Distributed Systems with Modular, Bounded Reasoning

Roopsha Samanta, Nouraldin Jaber, Christopher Wagner

Build your own optimizer with egg!

Max Willsey, Zachary Tatlock

22:40

Mech: An Array Programming Language for Robots (extended abstract)

23:00

InfERL: Scalable and extensible static analysis for Erlang

Productivity Assessment of Neural Code Completion

Albert Ziegler, Eirini Kalliamvakou, X. Alice Li, Andrew Rice, Devon Rifkin, Shawn Simister, Ganesh Sittampalam, Eddie Aftandilian

Probabilistic Array Programming on Galois Fields (extended abstract)

Breandan Considine, Jin L.C. Guo, Xujie Si

23:20

Predictive Synthesis of API-Centric Code

Daye Nam, Baishakhi Ray, Seohyun Kim, xianshan qu, Satish Chandra

Parallel Scan As a Multidimensional Array Problem

Artjoms Šinkarovs, Sven-Bodo Scholz

23:40

From Perception to Programs: Regularize, Overparameterize, and Amortize

Hao Tang, Kevin Ellis

Tue 14 Jun

0:00

Tue 14 Jun
Displayed time zone: Pacific Time (US & Canada) change

Tue 14 Jun

Rousseau Center

1:20

Can Transformers Code?

Your Research and Everyone Else

Martin C. Rinard

Combinatory Logic and Combinators in Array Languages

Reasoning About and Discovering LLVM Optimizations

John Regehr, Nuno P. Lopes

Finding Real Bugs in Big Programs with Incorrectness Logic

Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, Peter W. O'Hearn

Filling the gap between the JavaScript language specification and tools using the JISET family

Sukyoung Ryu, Jihyeok Park, Seungmin An

1:40

From Functional to Imperative: Combining Destination-Passing Style and Views

Zhitao Lin, Christophe Dubach

2:00

Syntax-Guided Program Reduction for Understanding Neural Code Intelligence Models

Rafiqul Rabin, Aftab Hussain, Amin Alipour

2:20

HIPPODROME: Data Race Repair using Static Analysis Summaries

Andreea Costea, Abhishek Tiwari, Sigmund Chianasta, Kishore R, Abhik Roychoudhury, Ilya Sergey

A Systematic Evaluation of Large Language Models of Code

Frank F. Xu, Uri Alon, Graham Neubig, Vincent J. Hellendoorn

Using Q-Learning to Select the Best Among Functionally Equivalent Implementations

Meggie van den Oever, Lauren Grimley, Richard Veras

2:40

Poster Session

3:00

3:20

Unsupervised Program Synthesis: Hierarchy and Perception

How to Write a Technical Paper

Reasoning About and Discovering LLVM Optimizations

John Regehr, Nuno P. Lopes

Infer#’s journey to bring Infer to the .NET world

Xin Shi, Xiaoyu Liu, Matthew Jin, Neel Sundaresan

Filling the gap between the JavaScript language specification and tools using the JISET family

Sukyoung Ryu, Jihyeok Park, Seungmin An

3:40

4:00

ExeBench: An ML-scale dataset of executable C functions

Jordi Armengol-Estapé, Jackson Woodruff, Alexander Brauckmann, José Wesley de Souza Magalhães, Michael F. P. O'Boyle

4:20

Infer in the cloud: An Overview of Infer Usage via Sonatype Lift

Rishav Mishra, Stephen Magill

Automatically Debugging AutoML Pipelines Using Maro: ML Automated Remediation Oracle

Julian Dolby, Jason Tsay, Martin Hirzel

4:40

A Graph Neural Network-based performance model for Deep Learning Applications

Shikhar Singh, James Hegarty, Hugh Leather, Benoit Steiner

5:00

5:20

5:40

6:00

6:20

6:40

7:00

7:20

7:40

8:00

8:20

8:40

9:00

+12hProgram Analysis for the Optimization and Verification of (Ethereum) Smart Contracts

+12hA Research Mindset

Kathryn S McKinley

+12hDomain-specific programming methodologies for domain-specific and emerging computing systems

Jeronimo Castrillon

+12hSketch-Guided Equality Saturation

9:20

+12hSynthesizing Mathematical Identities with E-graphs

Ian Briggs, Pavel Panchekha

9:40

10:00

+12hWelcome from the Chairs and Conference Report

David Chisnall, Michael Lippautz

10:20

+12hAbstract interpretation of Michelson smart-contracts

Guillaume Bau, Antoine Miné, Vincent Botbol, Mehdi Bouaziz

Safety Proof Simplification Through Commutativity

+12hMentoring Panel: Post-graduate Career Paths

Michael Greenberg, Chris Hawblitzel, Hila Peleg, Sukyoung Ryu, Deian Stefan

+12hBlack Box Static Analyses with Deep Learning

Miltiadis Allamanis

+12hRollBin: Reducing code-size via loop rerolling at binary level

Tianao Ge, Zewei Mo, Kan Wu, Xianwei Zhang, Yutong Lu

+12hIndustry panel: Memory management priorities for the next few years

Nathaniel Wesley Filardo, Chris Kennelly, Christine H. Flood

+12hLogging an Egg: Datalog on E-Graphs

10:40

+12hChasing an egg

+12hTighten Rust's Belt: Shrinking Embedded Rust Binaries

Hudson Ayers, Evan Laufer, Paul Mure, Jaehyeon Park, Eduardo Rodelo, Thea Rossman, Andrey Pronin, Philip Levis, Johnathan Van Why

+12hBinFPE: Accurate Floating-Point Exception Detection for GPU Applications

Ignacio Laguna, Xinyi Li, Ganesh Gopalakrishnan

11:00

+12hECTAs: E-Graphs Better (at Encoding)

James Koppel, Zheng Guo, Edsko de Vries, Armando Solar-Lezama, Nadia Polikarpova

Commutativity and Approximate Computing

Martin C. Rinard

+12hJAX Based Parallel Inference for Reactive Probabilistic Programming

Guillaume Baudart, Louis Mandel, Reyyan Tekin

+12hBalancing the use of ML and Program Analysis for Bug finding

+12hE-Graphs, VSAs, and Tree Automata: a Rosetta Stone

Yisu Remy Wang, James Koppel, Altan Haan, Josh Pollock

11:20

+12hTowards an Implementation of Differential Dynamic Logic in PVS

J Tanner Slagel, César Muñoz, Swee Balachandran, Mariano Moscato, Aaron Dutle, Paolo Masci, Lauren White

+12hImplicit State Machines

Fengyun Liu, Aleksandar Prokopec

+12hReconsidering OS Memory Optimizations in the Presence of Disaggregated Memory

Shai Bergman, Priyank Faldu, Boris Grot, Lluís Vilanova, Mark Silberstein

+12hEquality Saturation as a Tactic for Proof Assistants

Andrés Goens, Siddharth Bhat

11:40

+12hStatically Detecting Data Leakages in Data Science Code

Pavle Subotic, Uros Bojanic, Milan Stojic

+12hTowards Optimising Certified Programs by Proof Rewriting

Kiran Gopinathan, Ilya Sergey

Lightning: Extending Commutativity via Safe Abstraction

+12h(WIP) Scalable Size Inliner for Mobile Applications

12:00

12:20

12:40

13:00

13:20

+12hStatic Analysis for Data Scientists

Weakening Mazurkiewicz Traces

+12hWhose Life Are You Making Better

+12hThinking Like a Developer? Comparing the Attention of Humans with Neural Models of Code

+12hOptimizing Data Reshaping Operations in Functional IRs for High-Level Synthesis

Christof Schlaak, Tzung-Han Juang, Christophe Dubach

13:40

+12hCo-Mining: A Processing-in-Memory Assisted Framework for Memory-Intensive PoW Acceleration

Tianyu Wang, Zhaoyan Shen, Zili Shao

14:00

+12hMemSweeper: Virtualizing Cluster Memory Management for High Memory Utilization and Isolation

AmirHossein Seyri, Abhisek Pan, Balajee Vamanan

+12hQuiche: A Python Implementation of E-Graphs

Mergeable Replicated Datatypes

Suresh Jagannathan

+12hISKEVA: In-SSD Key-Value Database Engine for Video Analytics Applications

Yi Zheng, Joshua Fixelle, ‪Nagadastagiri Challapalle‬, Pingyi Huo, Vijaykrishnan Narayanan, Zili Shao, Mircea R. Stan, Zhaoyan Shen

+12hProgram Synthesis, Program Semantics, and Large Language Models

+12hOptimizing Large Integer Multiplier on FPGAs Using Equality Saturation

Ecenur Ustun, Jiaqi Yin, Zhiru Zhang

14:20

+12hEnsuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report

Luca Olivieri, Fabio Tagliaferro, Vincenzo Arceri, Marco Ruaro, Luca Negrini, Agostino Cortesi, Pietro Ferrara, Fausto Spoto, Enrico Talin

+12hAn Old Friend Is Better Than Two New Ones: Dual-Screen Android

Zizhan Chen, Siqi Shang, Qihong Wu, Jin Xue, Zhaoyan Shen, Zili Shao

+12hReplication-based Object Persistence by Reachability

Kotaro Matsumoto, Tomoharu Ugawa, Hideya Iwasaki

+12hWasm-mutate: Fuzzing WebAssembly Compilers with E-Graphs

Javier Cabrera Arteaga, Nicholas Fitzgerald, Martin Monperrus, Benoit Baudry

14:40

+12hQuEgg: Automatic Optimization of Quantum Circuits Using Equality Graphs

Lightning-4

+12h(WIP) Cache-Coherent CLAM

15:00

+12hConcurrent and Parallel Garbage Collection for Lightweight Threads on Multicore Processors

Katsuhiro Ueno, Atsushi Ohori

15:20

+12hUsing static analysis to scale security at Meta

Francesco Logozzo

Testing Distributed Protocols using Communication Closure

Constantin Enea

+12hMentoring Panel: Hot Topics in PL

Michael Carbin, Andrew Myers, Nadia Polikarpova, Limin Jia, Nikhil Swamy

+12hAutomated Software Testing: Bridging The Gap With Deep Learning

Elizabeth Dinella

+12hCode Generation Criteria for Buffered Exposed Datapath Architectures from Dataflow Graphs

Klaus Schneider, Anoop Bhagyanath, Julius Roob

+12hSocial break

+12hOn the Optimization of Equivalent Concurrent Computations

Henrich Lauko, Lukáš Korenčik, Peter Goodman

15:40

+12hAbstract Interpretation on E-Graphs

Samuel Coward, George A. Constantinides, Theo Drane

+12hTrace-and-Brace (TAB): Bespoke Software Countermeasures against Soft Errors

Yousun Ko, Alex Bradbury, Bernd Burgstaller, Robert Mullins

16:00

+12hWe Live in Interesting Times

Steve Blackburn

+12hColored E-Graph: Supporting Multiple Equivalence Relations with Resource Sharing

Eytan Singher, Shachar Itzhaky

Pretend synchrony: synchronous verification of asynchronous distributed programs

Klaus v. Gleissenthall

+12hAutomated Kernel Fusion for GPU Based on Code Motion

Junji Fukuhara, Munehiro Takimoto

+12hPrecise Program Reasoning using Probabilistic Methods

Mukund Raghothaman

+12hToward a Unified Framework for Program Optimization, Bug-Finding, and Repair

Jordan Schmerge, Jake Vossen, Jedidiah McClurg

16:20

+12hADA: A Tool for Visualizing The Architectural Overview of Open-Source Repositories

Md Rakib Hossain Misu, Aleksandar Saša Janjanin, Zhiqiang Bian, Valentin-Sebastian Burlacu, Naum Anteski

+12hTCPS: A Task and Cache-aware Partitioned Scheduler for Hard Real-time Multi-core Systems

Yixian Shen, Jun Xiao, Andy Pimentel

16:40

Closing Remarks & Business Meeting

Eric Koskinen, Azadeh Farzan, Constantin Enea

+12h(WIP) A Memory Interference Analysis using a Formal Timing Analyzer

+12hModeling Code Manipulation in JIT Compilers

HeuiChan Lim, Xiyu Kang, Saumya Debray

17:00

+12hClosing Remarks

David Chisnall, Michael Lippautz

17:20

17:40

18:00

18:20

18:40

19:00

19:20

19:40

20:00

20:20

20:40

21:00

Program Analysis for the Optimization and Verification of (Ethereum) Smart Contracts

A Research Mindset

Kathryn S McKinley

Domain-specific programming methodologies for domain-specific and emerging computing systems

Jeronimo Castrillon

Sketch-Guided Equality Saturation

21:20

Synthesizing Mathematical Identities with E-graphs

Ian Briggs, Pavel Panchekha

21:40

22:00

Welcome from the Chairs and Conference Report

David Chisnall, Michael Lippautz

22:20

Abstract interpretation of Michelson smart-contracts

Guillaume Bau, Antoine Miné, Vincent Botbol, Mehdi Bouaziz

Mentoring Panel: Post-graduate Career Paths

Michael Greenberg, Chris Hawblitzel, Hila Peleg, Sukyoung Ryu, Deian Stefan

Black Box Static Analyses with Deep Learning

Miltiadis Allamanis

RollBin: Reducing code-size via loop rerolling at binary level

Tianao Ge, Zewei Mo, Kan Wu, Xianwei Zhang, Yutong Lu

Industry panel: Memory management priorities for the next few years

Nathaniel Wesley Filardo, Chris Kennelly, Christine H. Flood

Logging an Egg: Datalog on E-Graphs

22:40

Chasing an egg

Tighten Rust's Belt: Shrinking Embedded Rust Binaries

Hudson Ayers, Evan Laufer, Paul Mure, Jaehyeon Park, Eduardo Rodelo, Thea Rossman, Andrey Pronin, Philip Levis, Johnathan Van Why

BinFPE: Accurate Floating-Point Exception Detection for GPU Applications

Ignacio Laguna, Xinyi Li, Ganesh Gopalakrishnan

23:00

ECTAs: E-Graphs Better (at Encoding)

James Koppel, Zheng Guo, Edsko de Vries, Armando Solar-Lezama, Nadia Polikarpova

JAX Based Parallel Inference for Reactive Probabilistic Programming

Guillaume Baudart, Louis Mandel, Reyyan Tekin

Balancing the use of ML and Program Analysis for Bug finding

E-Graphs, VSAs, and Tree Automata: a Rosetta Stone

Yisu Remy Wang, James Koppel, Altan Haan, Josh Pollock

23:20

Towards an Implementation of Differential Dynamic Logic in PVS

J Tanner Slagel, César Muñoz, Swee Balachandran, Mariano Moscato, Aaron Dutle, Paolo Masci, Lauren White

Implicit State Machines

Fengyun Liu, Aleksandar Prokopec

Reconsidering OS Memory Optimizations in the Presence of Disaggregated Memory

Shai Bergman, Priyank Faldu, Boris Grot, Lluís Vilanova, Mark Silberstein

Equality Saturation as a Tactic for Proof Assistants

Andrés Goens, Siddharth Bhat

23:40

Statically Detecting Data Leakages in Data Science Code

Pavle Subotic, Uros Bojanic, Milan Stojic

Towards Optimising Certified Programs by Proof Rewriting

Kiran Gopinathan, Ilya Sergey

(WIP) Scalable Size Inliner for Mobile Applications

Wed 15 Jun

0:00

Wed 15 Jun
Displayed time zone: Pacific Time (US & Canada) change

Wed 15 Jun

Backyard Kitchen & Tap

PLTea (Virtual see event for Zoom)

Rousseau Center

Wed 15 Jun

0:00

0:20

0:40

1:00

1:20

Static Analysis for Data Scientists

Whose Life Are You Making Better

Thinking Like a Developer? Comparing the Attention of Humans with Neural Models of Code

Optimizing Data Reshaping Operations in Functional IRs for High-Level Synthesis

Christof Schlaak, Tzung-Han Juang, Christophe Dubach

1:40

Co-Mining: A Processing-in-Memory Assisted Framework for Memory-Intensive PoW Acceleration

Tianyu Wang, Zhaoyan Shen, Zili Shao

2:00

MemSweeper: Virtualizing Cluster Memory Management for High Memory Utilization and Isolation

AmirHossein Seyri, Abhisek Pan, Balajee Vamanan

Quiche: A Python Implementation of E-Graphs

ISKEVA: In-SSD Key-Value Database Engine for Video Analytics Applications

Yi Zheng, Joshua Fixelle, ‪Nagadastagiri Challapalle‬, Pingyi Huo, Vijaykrishnan Narayanan, Zili Shao, Mircea R. Stan, Zhaoyan Shen

Program Synthesis, Program Semantics, and Large Language Models

Optimizing Large Integer Multiplier on FPGAs Using Equality Saturation

Ecenur Ustun, Jiaqi Yin, Zhiru Zhang

2:20

Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report

Luca Olivieri, Fabio Tagliaferro, Vincenzo Arceri, Marco Ruaro, Luca Negrini, Agostino Cortesi, Pietro Ferrara, Fausto Spoto, Enrico Talin

An Old Friend Is Better Than Two New Ones: Dual-Screen Android

Zizhan Chen, Siqi Shang, Qihong Wu, Jin Xue, Zhaoyan Shen, Zili Shao

Replication-based Object Persistence by Reachability

Kotaro Matsumoto, Tomoharu Ugawa, Hideya Iwasaki

Wasm-mutate: Fuzzing WebAssembly Compilers with E-Graphs

Javier Cabrera Arteaga, Nicholas Fitzgerald, Martin Monperrus, Benoit Baudry

2:40

QuEgg: Automatic Optimization of Quantum Circuits Using Equality Graphs

(WIP) Cache-Coherent CLAM

3:00

Concurrent and Parallel Garbage Collection for Lightweight Threads on Multicore Processors

Katsuhiro Ueno, Atsushi Ohori

3:20

Using static analysis to scale security at Meta

Francesco Logozzo

Mentoring Panel: Hot Topics in PL

Michael Carbin, Andrew Myers, Nadia Polikarpova, Limin Jia, Nikhil Swamy

Automated Software Testing: Bridging The Gap With Deep Learning

Elizabeth Dinella

Code Generation Criteria for Buffered Exposed Datapath Architectures from Dataflow Graphs

Klaus Schneider, Anoop Bhagyanath, Julius Roob

Social break

On the Optimization of Equivalent Concurrent Computations

Henrich Lauko, Lukáš Korenčik, Peter Goodman

3:40

Abstract Interpretation on E-Graphs

Samuel Coward, George A. Constantinides, Theo Drane

Trace-and-Brace (TAB): Bespoke Software Countermeasures against Soft Errors

Yousun Ko, Alex Bradbury, Bernd Burgstaller, Robert Mullins

4:00

We Live in Interesting Times

Steve Blackburn

Colored E-Graph: Supporting Multiple Equivalence Relations with Resource Sharing

Eytan Singher, Shachar Itzhaky

Automated Kernel Fusion for GPU Based on Code Motion

Junji Fukuhara, Munehiro Takimoto

Precise Program Reasoning using Probabilistic Methods

Mukund Raghothaman

Toward a Unified Framework for Program Optimization, Bug-Finding, and Repair

Jordan Schmerge, Jake Vossen, Jedidiah McClurg

4:20

ADA: A Tool for Visualizing The Architectural Overview of Open-Source Repositories

Md Rakib Hossain Misu, Aleksandar Saša Janjanin, Zhiqiang Bian, Valentin-Sebastian Burlacu, Naum Anteski

TCPS: A Task and Cache-aware Partitioned Scheduler for Hard Real-time Multi-core Systems

Yixian Shen, Jun Xiao, Andy Pimentel

4:40

(WIP) A Memory Interference Analysis using a Formal Timing Analyzer

Modeling Code Manipulation in JIT Compilers

HeuiChan Lim, Xiyu Kang, Saumya Debray

5:00

Closing Remarks

David Chisnall, Michael Lippautz

5:20

5:40

6:00

6:20

6:40

7:00

7:20

7:40

8:00

8:20

8:40

9:00

+12hWelcome to PLDI 2022

Işıl Dillig, Ranjit Jhala

+12hGetting Your Research Adopted

Emery D. Berger

9:20

9:40

10:00

10:20

10:40

(ICFP 2020) TLC: Temporal Logic of Distributed Components

Jeremiah Griffin, Mohsen Lesani, Narges Shadab, Xizhe Yin

+12hP4BID: Information Flow Control in P4

Karuna Grewal, Loris D'Antoni, Justin Hsu

(OOPSLA 2020) Perfectly Parallel Fairness Certification of Neural Networks

Caterina Urban, Maria Christakis, Valentin Wüstholz, Fuyuan Zhang

+12hIs it Time to Retire Manual Concurrent Memory Reclamation?

Daniel Anderson, Guy E. Blelloch, Yuanhao Wei

11:00

(OOPSLA 2021) Durable functions: semantics for stateful serverless

Sebastian Burckhardt, Chris Gillum, David Justo, Konstantinos Kallas, Connor McMahon, Christopher Meiklejohn

+12hANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification

Sankha Narayan Guria, Niki Vazou, Marco Guarnieri, James Parker

(PLDI 2020) OOElala : Order-Of-Evaluation based Alias Analysis for compiler optimization

Ankush Phulia, Vaibhav Bhagee, Sorav Bansal

+12hLow-Latency, High-Throughput Garbage Collection

Wenyu Zhao, Steve Blackburn, Kathryn S McKinley

Distinguished Paper Award

11:20

(OOPSLA 2021) ECROs: building global scale systems from sequential code

Kevin De Porre, Carla Ferreira, Nuno Preguica, Elisa Gonzalez Boix

+12hHardening Attack Surfaces with Formally Proven Binary Format Parsers

Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, Arti Gupta

(POPL 2021) Simplifying Dependent Reductions with the Polyhedral Model

Cambridge Yang, Eric Atkinson, Michael Carbin

+12hMako: A Low-Pause, High-Throughput Evacuating Collector for Memory-Disaggregated Datacenters

Haoran Ma, Shi Liu, Chenxi Wang, Yifan Qiao, Michael D. Bond, Steve Blackburn, Miryung Kim, Guoqing Harry Xu

11:40

(POPL 2022) Induction Duality: Primal-Dual Search for Invariants

Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, Alex Aiken

+12hModular Information Flow Through Ownership

Will Crichton, Marco Patrignani, Maneesh Agrawala, Pat Hanrahan

(POPL 2021) The Fine-Grained and Parallel Complexity of Andersen's Pointer Analysis

Andreas Pavlogiannis, Anders Alnor Mathiasen

+12hPaC-trees: Supporting Parallel and Compressed Purely-Functional Collections

Laxman Dhulipala, Guy E. Blelloch, Yan Gu, Yihan Sun

12:00

12:20

12:40

13:00

13:20

(POPL 2021) Petr4: Formal Foundations for P4 Data Planes

Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, Nate Foster

+12hWebRobot: Web Robotic Process Automation using Interactive Programming-by-Demonstration

Rui Dong, Zhicheng Huang, Ian Iong Lam, Yan Chen, Xinyu Wang

(OOPSLA 2021) Reconciling Optimization with Secure Compilation

Son Tuan Vu, Albert Cohen, Arnaud de Grandmaison, Christophe Guillon, Karine Heydemann

+12hFinding Typing Compiler Bugs

Stefanos Chaliasos, Thodoris Sotiropoulos, Diomidis Spinellis, Arthur Gervais, Ben Livshits, Dimitris Mitropoulos

Distinguished Paper Award

13:40

(PLDI 2020) Predictable Accelerator Design with Time-Sensitive Affine Types

Rachit Nigam, Sachille Atapattu, Samuel Thomas, Theodore Bauer, Apurva Koti, Zhijing Li, Yuwei Ye, Adrian Sampson, Zhiru Zhang

+12hSynthesizing Analytical SQL Queries from Computation Demonstration

Xiangyu Zhou, Rastislav Bodík, Alvin Cheung, Chenglong Wang

Distinguished Paper Award

(PLDI 2020) Constant-Time Foundations for the New Spectre Era

Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, Gilles Barthe

+12hIRDL: An IR Definition Language for SSA Compilers

Mathieu Fehr, Jeff Niu, River Riddle, Mehdi Amini, Zhendong Su, Tobias Grosser

14:00

(POPL 2022) Dependently-Typed Data Plane Programming

Matthias Eichholz, Eric Campbell, Matthias Krebs, Nate Foster, Mira Mezini

+12hType-Directed Program Synthesis for RESTful APIs

Zheng Guo, David Cao, Davin Tjong, Jean Yang, Cole Schlesinger, Nadia Polikarpova

(PLDI 2020) SCAF: A Speculation-Aware Collaborative Dependence Analysis Framework

Sotiris Apostolakis, Ziyang Xu, Zujun Tan, Greg Chan, Simone Campanoni, David I. August

+12hSequential Reasoning for Optimizing Compilers Under Weak Memory Concurrency

Minki Cho, Sung-Hwan Lee, Dongjae Lee, Chung-Kil Hur, Ori Lahav

14:20

(POPL 2022) Safe, Modular Packet Pipeline Programming

Devon Loehr, David Walker

+12hVisualization Question Answering Using Introspective Program Synthesis

Yanju Chen, Xifeng Yan, Yu Feng

Distinguished Paper Award

(POPL 2021) Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade

Marco Vassena, Craig Disselkoen, Klaus v. Gleissenthall, Sunjay Cauligi, Rami Gökhan Kıcı, Ranjit Jhala, Dean Tullsen, Deian Stefan

+12hDeoptless: Speculation with Dispatched On-Stack Replacement and Specialized Continuations

Olivier Flückiger, Jan Ječmen, Sebastián Krynski, Jan Vitek

14:40

15:00

15:20

(PLDI 2020) Inductive Sequentialization of Asynchronous Programs

Constantin Enea, Thomas A. Henzinger, Bernhard Kragl, Suha Orhun Mutluergil, Shaz Qadeer

+12hCan Reactive Synthesis and Syntax-Guided Synthesis Be Friends?

Wonhyuk Choi, Bernd Finkbeiner, Ruzica Piskac, Mark Santolucito

(OOPSLA 2021) FPL: fast Presburger arithmetic through transprecision

Arjun Pitchanathan, Christian Ulmann, Michel Weber, Torsten Hoefler, Tobias Grosser

+12hAutoscheduling for Sparse Tensor Algebra with an Asymptotic Cost Model

Peter Ahrens, Fredrik Kjolstad, Saman Amarasinghe

15:40

(PLDI 2021) When Threads Meet Events: Efficient and Precise Static Race Detection with Origins

Bozhen Liu, Peiming Liu, Yanze Li, Chia-Che Tsai, Dilma Da Silva, Jeff Huang

+12hRecursion Synthesis with Unrealizability Witnesses

Azadeh Farzan, Danya Lette, Victor Nicolet

(PLDI 2021) Provable Repair of Deep Neural Networks

Matthew Sotoudeh, Aditya V. Thakur

+12hDISTAL: The Distributed Tensor Algebra Compiler

Rohan Yadav, Alex Aiken, Fredrik Kjolstad

16:00

(POPL 2021) Optimal Prediction of Synchronization-Preserving Races

Umang Mathur, Andreas Pavlogiannis, Mahesh Viswanathan

+12hTF-Coder: Program Synthesis for Tensor Manipulations (TOPLAS)

Kensen Shi, David Bieber, Rishabh Singh

(POPL 2022) One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding Modes

Jay P. Lim, Santosh Nagarakatte

+12hAll you need is Superword-Level Parallelism: Systematic Control-Flow Vectorization with SLP

Yishen Chen, Charith Mendis, Saman Amarasinghe

16:20

(POPL 2022) Visibility Reasoning for Concurrent Snapshot Algorithms

Joakim Öhman, Aleksandar Nanevski

+12h“Synthesizing Input Grammars”: A Replication Study

Bachir Bendrissou, Rahul Gopinath, Andreas Zeller

(POPL 2022) Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation

Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, Andrew Fitzgibbon

+12hWarping Cache Simulation of Polyhedral Programs

Canberk Morelli, Jan Reineke

16:40

+12hResponse by authors of "Synthesizing Input Grammars"

17:00

Designing for ABI-Stable Software Evolution in the Swift Programming Language

17:20

Meta Research and Opportunities

Francesco Logozzo

Overlapping Events:

Control Logic Synthesis Using Formal ISA Specifications

Coupled Applicative Functors

Program Synthesis for Processor Development Using Formal Specifications

Path Alignment Automata are Probabilistic Couplings

Multi-Phase Invariant Synthesis

Finding Good Generators with Multi-Armed Bandits

Impacts of Range Reduction on Polynomial Approximation Efficiency

Automating NISQ Application Design with Meta Quantum Circuits with Constraints (MQCC)

A Type System for Safe Intermittent Computing

PBUnit: A Live Programming Environment for Unit Testing

Visualization with Refinement Types

PLDI 2022 Reception (sponsored by WhatsApp by Meta)

17:40

18:00

18:20

18:40

19:00

W@PLDI Dinner

19:20

19:40

20:00

20:20

20:40

21:00

Welcome to PLDI 2022

Işıl Dillig, Ranjit Jhala

Getting Your Research Adopted

Emery D. Berger

21:20

21:40

22:00

22:20

22:40

P4BID: Information Flow Control in P4

Karuna Grewal, Loris D'Antoni, Justin Hsu

Is it Time to Retire Manual Concurrent Memory Reclamation?

Daniel Anderson, Guy E. Blelloch, Yuanhao Wei

23:00

ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification

Sankha Narayan Guria, Niki Vazou, Marco Guarnieri, James Parker

Low-Latency, High-Throughput Garbage Collection

Wenyu Zhao, Steve Blackburn, Kathryn S McKinley

Distinguished Paper Award

23:20

Hardening Attack Surfaces with Formally Proven Binary Format Parsers

Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, Arti Gupta

Mako: A Low-Pause, High-Throughput Evacuating Collector for Memory-Disaggregated Datacenters

Haoran Ma, Shi Liu, Chenxi Wang, Yifan Qiao, Michael D. Bond, Steve Blackburn, Miryung Kim, Guoqing Harry Xu

23:40

Modular Information Flow Through Ownership

Will Crichton, Marco Patrignani, Maneesh Agrawala, Pat Hanrahan

PaC-trees: Supporting Parallel and Compressed Purely-Functional Collections

Laxman Dhulipala, Guy E. Blelloch, Yan Gu, Yihan Sun

Thu 16 Jun

0:00

Thu 16 Jun
Displayed time zone: Pacific Time (US & Canada) change

Thu 16 Jun

PLTea (Virtual see event for Zoom)

1:20

WebRobot: Web Robotic Process Automation using Interactive Programming-by-Demonstration

Rui Dong, Zhicheng Huang, Ian Iong Lam, Yan Chen, Xinyu Wang

Finding Typing Compiler Bugs

Stefanos Chaliasos, Thodoris Sotiropoulos, Diomidis Spinellis, Arthur Gervais, Ben Livshits, Dimitris Mitropoulos

Distinguished Paper Award

1:40

Synthesizing Analytical SQL Queries from Computation Demonstration

Xiangyu Zhou, Rastislav Bodík, Alvin Cheung, Chenglong Wang

Distinguished Paper Award

IRDL: An IR Definition Language for SSA Compilers

Mathieu Fehr, Jeff Niu, River Riddle, Mehdi Amini, Zhendong Su, Tobias Grosser

2:00

Type-Directed Program Synthesis for RESTful APIs

Zheng Guo, David Cao, Davin Tjong, Jean Yang, Cole Schlesinger, Nadia Polikarpova

Sequential Reasoning for Optimizing Compilers Under Weak Memory Concurrency

Minki Cho, Sung-Hwan Lee, Dongjae Lee, Chung-Kil Hur, Ori Lahav

2:20

Visualization Question Answering Using Introspective Program Synthesis

Yanju Chen, Xifeng Yan, Yu Feng

Distinguished Paper Award

Deoptless: Speculation with Dispatched On-Stack Replacement and Specialized Continuations

Olivier Flückiger, Jan Ječmen, Sebastián Krynski, Jan Vitek

2:40

3:00

3:20

Can Reactive Synthesis and Syntax-Guided Synthesis Be Friends?

Wonhyuk Choi, Bernd Finkbeiner, Ruzica Piskac, Mark Santolucito

Autoscheduling for Sparse Tensor Algebra with an Asymptotic Cost Model

Peter Ahrens, Fredrik Kjolstad, Saman Amarasinghe

3:40

Recursion Synthesis with Unrealizability Witnesses

Azadeh Farzan, Danya Lette, Victor Nicolet

DISTAL: The Distributed Tensor Algebra Compiler

Rohan Yadav, Alex Aiken, Fredrik Kjolstad

4:00

TF-Coder: Program Synthesis for Tensor Manipulations (TOPLAS)

Kensen Shi, David Bieber, Rishabh Singh

All you need is Superword-Level Parallelism: Systematic Control-Flow Vectorization with SLP

Yishen Chen, Charith Mendis, Saman Amarasinghe

4:20

“Synthesizing Input Grammars”: A Replication Study

Bachir Bendrissou, Rahul Gopinath, Andreas Zeller

Warping Cache Simulation of Polyhedral Programs

Canberk Morelli, Jan Reineke

4:40

Response by authors of "Synthesizing Input Grammars"

5:00

5:20

5:40

6:00

6:20

6:40

7:00

7:20

7:40

8:00

8:20

8:40

9:00

+12hThe PLDI Song

John Wickerson, Alastair F. Donaldson

+12h Imposter Syndrome, Stupid Questions, and Eight (+/-2) Problems I Need your Help With

9:20

9:40

10:00

10:20

10:40

(PLDI 2021) DreamCoder: Bootstrapping inductive program synthesis with wake-sleep library learning

Kevin Ellis, Lionel Wong, Maxwell Nye, Mathias Sablé-Meyer, Lucas Morales, Luke Hewitt, Luc Cary, Armando Solar-Lezama, Joshua B. Tenenbaum

+12hCertified Mergeable Replicated Data Types

Vimala Soundarapandian, Adharsh Kamath, Kartik Nagar, KC Sivaramakrishnan

(ICFP 2021) Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model

Glen Mével, Jacques-Henri Jourdan

+12hCycleQ: an efficient basis for cyclic equational reasoning

Eddie Jones, C.-H. Luke Ong, Steven Ramsay

11:00

(POPL 2021) egg: Fast and Extensible Equality Saturation

Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, Pavel Panchekha

+12hHamband: RDMA Replicated Data Types

Farzin Houshmand, Javad Saberlatibari, Mohsen Lesani

(PLDI 2020) Zippy LL(1) Parsing with Derivatives

Romain Edelmann, Jad Hamza, Viktor Kunčak

+12hFinding the Dwarf: Recovering Precise Types from WebAssembly Binaries

Daniel Lehmann, Michael Pradel

11:20

(POPL 2022) Relational E-Matching

Yihong Zhang, Yisu Remy Wang, Max Willsey, Zachary Tatlock

+12hRunTime-Assisted Convergence in Replicated Data Types

Gowtham Kaki, Prasanth Prahladan, Nicholas V. Lewchenko

(PLDI 2021) CoStar: A Verified ALL(*) Parser

Sam Lasser, Chris Casinghino, Kathleen Fisher, Cody Roux

+12hAbstract Interpretation Repair

Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Francesco Ranzato

11:40

(OOPSLA 2020) Just-in-Time Learning for Bottom-up Enumerative Synthesis

Shraddha Barke, Hila Peleg, Nadia Polikarpova

+12hAdore: Atomic Distributed Objects with Certified Reconfiguration

Wolf Honore, Ji-Yong Shin, Jieung Kim, Zhong Shao

(PLDI 2021) Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic

Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal

+12hDifferential Cost Analysis with Simultaneous Potentials and Anti-potentials

Đorđe Žikelić, Pauline Bolignano, Bor-Yuh Evan Chang, Franco Raimondi

12:00

12:20

12:40

13:00

13:20

(PLDI 2021) Phased Synthesis of Divide and Conquer Programs

Azadeh Farzan, Victor Nicolet

+12hA Flexible Type System for Fearless Concurrency

Mae Milano, Julia Turcotti, Andrew Myers

(ICFP 2020) Kinds Are Calling Conventions

Paul Downen, Zena M. Ariola, Simon Peyton Jones, Richard A. Eisenberg

+12hChoosing Mathematical Function Implementations for Speed and Accuracy

Ian Briggs, Pavel Panchekha

13:40

(OOPSLA 2021) LooPy: interactive program synthesis with control structures

Kasra Ferdowsi, Shraddha Barke, Hila Peleg, Sorin Lerner, Nadia Polikarpova

+12hA Study of Real-world Data Races in Golang

Milind Chabbi, Murali Krishna Ramanathan

(OOPSLA 2021) Study of the subtyping machine of nominal subtyping with variance

+12hGuaranteed bounds for posterior inference in universal probabilistic programming

Raven Beutner, C.-H. Luke Ong, Fabian Zaiser

14:00

(OOPSLA 2020) Feedback-Driven Semi-Supervised Synthesis of Program Transformations

Xiang Gao, Shraddha Barke, Arjun Radhakrishna, Gustavo Soares, Sumit Gulwani, Alan Leung, Nachiappan Nagappan, Ashish Tiwari

+12hChecking Robustness to Weak Persistency Models

Hamed Gorjiara, Weiyu Luo, Alex Lee, Guoqing Harry Xu, Brian Demsky

(POPL 2021) Fully Abstract from Static to Gradual

Koen Jacobs, Amin Timany, Dominique Devriese

+12hProgressive Polynomial Approximations for Fast Correctly Rounded Math Libraries

Mridul Aanjaneya, Jay P. Lim, Santosh Nagarakatte

14:20

(PLDI 2021) Proof Repair Across Type Equivalences

Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, Dan Grossman

+12hSound Sequentialization for Concurrent Program Verification

Azadeh Farzan, Dominik Klumpp, Andreas Podelski

(POPL 2021) On the Semantic Expressiveness of Recursive Types

Marco Patrignani, Eric Mark Martin, Dominique Devriese

+12hKarp: A Language for NP Reductions

Chenhao Zhang, Jason D. Hartline, Christos Dimoulas

14:40

15:00

15:20

(OOPSLA 2020) A Model for Detecting Faults in Build Specifications

Thodoris Sotiropoulos, Stefanos Chaliasos, Dimitris Mitropoulos, Diomidis Spinellis

+12hA Typed Continuation-Passing Translation for Lexical Effect Handlers

Philipp Schuster, Jonathan Immanuel Brachthäuser, Marius Müller, Klaus Ostermann

(PLDI 2020) Automatic Generation of Efficient Sparse Tensor Format Conversion Routines

Stephen Chou, Fredrik Kjolstad, Saman Amarasinghe

+12hQuartz: Superoptimization of Quantum Circuits

Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth, Henry Ma, Jens Palsberg, Alex Aiken, Umut A. Acar, Zhihao Jia

15:40

(OOPSLA 2020) Unifying Execution of Imperative Generators and Declarative Specifications

Pengyu Nie, Marinela Parovic, Zhiqiang Zang, Sarfraz Khurshid, Aleksandar Milicevic, Milos Gligoric

+12hDeep and Shallow Types for Gradual Languages

(PLDI 2020) NVTraverse: In NVRAM Data Structures, the Destination is More Important than the Journey

Naama Ben-David, Guy E. Blelloch, Michal Friedman, Erez Petrank, Yuanhao Wei

+12hGiallar: Push-button Verification for the Qiskit Quantum Compiler

Runzhou Tao, Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew Cross, Frederic T. Chong, Ronghui Gu

16:00

(PLDI 2021) Logical Bytecode Reduction

Christian Gram Kalhauge, Jens Palsberg

+12hKleene Algebra Modulo Theories: A Framework for Concrete KATs

Michael Greenberg, Ryan Beckett, Eric Campbell

Distinguished Paper Award

(PLDI 2021) Mirror: Making Lock-Free Data Structures Persistent

Michal Friedman, Erez Petrank, Pedro Ramalhete

+12hAlgebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra

Yuxiang Peng, Mingsheng Ying, Xiaodi Wu

16:20

(PLDI 2021) Quantum abstract interpretation

Nengkun Yu, Jens Palsberg

+12hSemantic Soundness for Language Interoperability

Daniel Patterson, Noble Mushtak, Andrew Wagner, Amal Ahmed

(POPL 2021) Provably Space Efficient Parallel Functional Programming

Jatin Arora, Sam Westrick, Umut A. Acar

+12hPyLSE: A Pulse-Transfer Level Language for Superconductor Electronics

Michael Christensen, Georgios Tzimpragos, Harlan Kringen, Jennifer Volk, Timothy Sherwood, Ben Hardekopf

16:40

17:00

17:20

17:40

18:00

18:20

18:40

19:00

19:20

19:40

20:00

20:20

20:40

21:00

The PLDI Song

John Wickerson, Alastair F. Donaldson

Imposter Syndrome, Stupid Questions, and Eight (+/-2) Problems I Need your Help With

21:20

21:40

22:00

22:20

22:40

Certified Mergeable Replicated Data Types

Vimala Soundarapandian, Adharsh Kamath, Kartik Nagar, KC Sivaramakrishnan

CycleQ: an efficient basis for cyclic equational reasoning

Eddie Jones, C.-H. Luke Ong, Steven Ramsay

23:00

Hamband: RDMA Replicated Data Types

Farzin Houshmand, Javad Saberlatibari, Mohsen Lesani

Finding the Dwarf: Recovering Precise Types from WebAssembly Binaries

Daniel Lehmann, Michael Pradel

23:20

RunTime-Assisted Convergence in Replicated Data Types

Gowtham Kaki, Prasanth Prahladan, Nicholas V. Lewchenko

Abstract Interpretation Repair

Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Francesco Ranzato

23:40

Adore: Atomic Distributed Objects with Certified Reconfiguration

Wolf Honore, Ji-Yong Shin, Jieung Kim, Zhong Shao

Differential Cost Analysis with Simultaneous Potentials and Anti-potentials

Đorđe Žikelić, Pauline Bolignano, Bor-Yuh Evan Chang, Franco Raimondi

Fri 17 Jun

0:00

Fri 17 Jun
Displayed time zone: Pacific Time (US & Canada) change

Fri 17 Jun

PLTea (Virtual see event for Zoom)

1:20

A Flexible Type System for Fearless Concurrency

Mae Milano, Julia Turcotti, Andrew Myers

Choosing Mathematical Function Implementations for Speed and Accuracy

Ian Briggs, Pavel Panchekha

1:40

A Study of Real-world Data Races in Golang

Milind Chabbi, Murali Krishna Ramanathan

Guaranteed bounds for posterior inference in universal probabilistic programming

Raven Beutner, C.-H. Luke Ong, Fabian Zaiser

2:00

Checking Robustness to Weak Persistency Models

Hamed Gorjiara, Weiyu Luo, Alex Lee, Guoqing Harry Xu, Brian Demsky

Progressive Polynomial Approximations for Fast Correctly Rounded Math Libraries

Mridul Aanjaneya, Jay P. Lim, Santosh Nagarakatte

2:20

Sound Sequentialization for Concurrent Program Verification

Azadeh Farzan, Dominik Klumpp, Andreas Podelski

Karp: A Language for NP Reductions

Chenhao Zhang, Jason D. Hartline, Christos Dimoulas

2:40

3:00

3:20

A Typed Continuation-Passing Translation for Lexical Effect Handlers

Philipp Schuster, Jonathan Immanuel Brachthäuser, Marius Müller, Klaus Ostermann

Quartz: Superoptimization of Quantum Circuits

Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth, Henry Ma, Jens Palsberg, Alex Aiken, Umut A. Acar, Zhihao Jia

3:40

Deep and Shallow Types for Gradual Languages

Giallar: Push-button Verification for the Qiskit Quantum Compiler

Runzhou Tao, Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew Cross, Frederic T. Chong, Ronghui Gu

4:00

Kleene Algebra Modulo Theories: A Framework for Concrete KATs

Michael Greenberg, Ryan Beckett, Eric Campbell

Distinguished Paper Award

Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra

Yuxiang Peng, Mingsheng Ying, Xiaodi Wu

4:20

Semantic Soundness for Language Interoperability

Daniel Patterson, Noble Mushtak, Andrew Wagner, Amal Ahmed

PyLSE: A Pulse-Transfer Level Language for Superconductor Electronics

Michael Christensen, Georgios Tzimpragos, Harlan Kringen, Jennifer Volk, Timothy Sherwood, Ben Hardekopf

4:40

5:00

5:20

5:40

6:00

6:20

6:40

7:00

7:20

7:40

8:00

8:20

8:40

9:00

+12hBusiness Meeting

Işıl Dillig, Ranjit Jhala, Steve Blackburn

9:20

9:40

10:00

10:20

10:40

(OOPSLA 2020) Scaling Exact Inference for Discrete Probabilistic Programs

Steven Holtzen, Guy Van den Broeck, Todd Millstein

+12hBind the Gap: Compiling Real Software to Hardware FFT Accelerators

Jackson Woodruff, Jordi Armengol-Estapé, Sam Ainsworth, Michael F. P. O'Boyle

(OOPSLA 2020) Counterexample-Guided Correlation Algorithm for Translation Validation

Shubhani Gupta, Abhishek Rose, Sorav Bansal

+12hSoftware-Hardware Codesign for Efficient In-Memory Regular Pattern Matching

Konstantinos Mamouras, Kaiyuan Yang, Lingkun Kong, Qixuan Yu, Agnishom Chattopadhyay, Alexis Le Glaunec, Yi Huang

11:00

(POPL 2021) A Pre-Expectation Calculus for Probabilistic Sensitivity

Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

+12hExocompilation for Productive Programming of Hardware Accelerators

Yuka Ikarashi, Gilbert Bernstein, Alex Reinking, Hasan Genc, Jonathan Ragan-Kelley

(OOPSLA 2021) Formal verification of high-level synthesis

Yann Herklotz, James D. Pollard, Nadesh Ramanathan, John Wickerson

11:20

(PLDI 2021) On Probabilistic Termination of Functional Programs with Continuous Distributions

Raven Beutner, C.-H. Luke Ong

+12hPDL: A High-Level Hardware Design Language for Pipelined Processors

Drew Zagieboylo, Charles Sherk, G. Edward Suh, Andrew Myers

(OOPSLA 2021) Well-typed programs can go wrong: a study of typing-related bugs in JVM compilers

Stefanos Chaliasos, Thodoris Sotiropoulos, Georgios-Petros Drosos, Charalambos Ioannis Mitropoulos, Dimitris Mitropoulos, Diomidis Spinellis

11:40

(POPL 2021) Paradoxes of probabilistic programming

+12hWARio: Efficient Code Generation for Intermittent Computing

Vito Kortbeek, Souradip Ghosh, Josiah Hester, Simone Campanoni, Przemysław Pawełczak

(POPL 2021) Formally Verified Speculation and Deoptimization in a JIT Compiler

Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, Jan Vitek

12:00

12:20

12:40

13:00

13:20

(POPL 2022) Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs

Charles Yuan, Christopher McNally, Michael Carbin

+12hCompass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic

Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, Derek Dreyer

(OOPSLA 2020) Automatic and Efficient Variability-Aware Lifting of Functional Programs

Ramy Shahin, Marsha Chechik

+12hEfficient Approximations for Cache-conscious Data Placement

Ali Ahmadi, Majid Daliri, Amir Kafshdar Goharshady, Andreas Pavlogiannis

13:40

(ICFP 2020) Compiling effect handlers in capability-passing style

Philipp Schuster, Jonathan Immanuel Brachthäuser, Klaus Ostermann

+12hDiaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris

Ike Mulder, Robbert Krebbers, Herman Geuvers

(OOPSLA 2021) Safer at Any Speed: Automatic Context-Aware Safety Enhancement for Rust

Natalie Popescu, Ziyang Xu, Sotiris Apostolakis, David I. August, Amit Levy

+12hFreeTensor: A Free-form DSL with Holistic Optimizations for Irregular Tensor Programs

Shizhi Tang, Jidong Zhai, Haojie Wang, Lin Jiang, Liyan Zheng, Zhenhao Yuan, Chen Zhang

14:00

(POPL 2021) Intensional Datatype Refinement

Eddie Jones, Steven Ramsay

+12hIslaris: Verification of Machine Code Against Authoritative ISA Semantics

Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell

(OOPSLA 2021) The semantics of shared memory in Intel CPU/FPGA systems

Dan Iorga, Alastair F. Donaldson, Tyler Sorensen, John Wickerson

+12hLasagne: A Static Binary Translator for Weak Memory Model Architectures

Rodrigo C. O. Rocha, Dennis Sprokholt, Martin Fink, Redha Gouicem, Tom Spink, Soham Chakraborty, Pramod Bhatotia

14:20

(POPL 2021) A Verified Optimizer for Quantum Circuits

Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks

+12hRustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code

Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer

Distinguished Paper Award

(PLDI 2020) Efficient Handling of String-Number Conversion

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Julian Dolby, Petr Janků, Hsin-Hung Lin, Lukáš Holík, Wei-Cheng Wu

+12hVerifying Optimizations of Concurrent Programs in the Promising Semantics

Junpeng Zha, Hongjin Liang, Xinyu Feng

14:40

15:00

15:20

(ICFP 2020) Achieving high-performance the functional way: a functional pearl on expressing high-performance optimizations as rewrite strategies

Bastian Hagedorn, Johannes Lenfers, Thomas Koehler, Xueying Qin, Sergei Gorlatch, Michel Steuwer

+12hRelational Compilation for Performance-Critical Applications

Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, Adam Chlipala

(OOPSLA 2020) Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell

Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, Niki Vazou

+12hInterpreter-guided Differential JIT Compiler Unit Testing

Guillermo Polito, Stéphane Ducasse, Pablo Tesone

15:40

(PLDI 2020) Optimizing Homomorphic Evaluation Circuits by Program Synthesis and Term Rewriting

DongKwon Lee, Woosuk Lee, Hakjoo Oh, Kwangkeun Yi

+12hFormally Verified Lifting of C-compiled x86-64 Binaries

Freek Verbeek, Joshua A. Bockenek, Zhoulai Fu, Binoy Ravindran

(PLDI 2021) RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types

Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg

+12hLandmarks and Regions: A Robust Approach to Data Extraction

Suresh Parthasarathy, Lincy Pattanaik, Anirudh Khatry, Arun Iyer, Arjun Radhakrishna, Sriram Rajamani, Mohammad Raza

16:00

(ICFP 2021) Grafs: Declarative Graph Analytics

Farzin Houshmand, Mohsen Lesani, Keval Vora

+12hLeapfrog: Certified Equivalence for Protocol Parsers

Ryan Doenges, Tobias Kappé, John Sarracino, Nate Foster, Greg Morrisett

(POPL 2021) Data Flow Refinement Type Inference

Zvonimir Pavlinovic, Yusen Su, Thomas Wies

+12hOdin: On-Demand Instrumentation with On-the-Fly Recompilation

Mingzhe Wang, Jie Liang, Chijin Zhou, Zhiyong Wu, Xinyi Xu, Yu Jiang

16:20

(POPL 2022) Verified Tensor-Program Optimization Via High-level Scheduling Rewrites

Amanda Liu, Gilbert Bernstein, Adam Chlipala, Jonathan Ragan-Kelley

+12hComputing Correctly with Inductive Relations

Zoe Paraskevopoulou, Aaron Eline, Leonidas Lampropoulos

(PLDI 2021) RbSyn: type- and effect-guided program synthesis

Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn

+12hQuickstrom: Property-based acceptance testing with LTL specifications

Liam O'Connor, Oskar Wickström

16:40

17:00

17:20

17:40

18:00

18:20

18:40

19:00

19:20

19:40

20:00

20:20

20:40

21:00

Business Meeting

Işıl Dillig, Ranjit Jhala, Steve Blackburn

21:20

21:40

22:00

22:20

22:40

Bind the Gap: Compiling Real Software to Hardware FFT Accelerators

Jackson Woodruff, Jordi Armengol-Estapé, Sam Ainsworth, Michael F. P. O'Boyle

Software-Hardware Codesign for Efficient In-Memory Regular Pattern Matching

Konstantinos Mamouras, Kaiyuan Yang, Lingkun Kong, Qixuan Yu, Agnishom Chattopadhyay, Alexis Le Glaunec, Yi Huang

23:00

Exocompilation for Productive Programming of Hardware Accelerators

Yuka Ikarashi, Gilbert Bernstein, Alex Reinking, Hasan Genc, Jonathan Ragan-Kelley

23:20

PDL: A High-Level Hardware Design Language for Pipelined Processors

Drew Zagieboylo, Charles Sherk, G. Edward Suh, Andrew Myers

23:40

WARio: Efficient Code Generation for Intermittent Computing

Vito Kortbeek, Souradip Ghosh, Josiah Hester, Simone Campanoni, Przemysław Pawełczak

Sat 18 Jun

0:00

Sat 18 Jun
Displayed time zone: Pacific Time (US & Canada) change

Sat 18 Jun

PLTea (Virtual see event for Zoom)

1:20

Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic

Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, Derek Dreyer

Efficient Approximations for Cache-conscious Data Placement

Ali Ahmadi, Majid Daliri, Amir Kafshdar Goharshady, Andreas Pavlogiannis

1:40

Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris

Ike Mulder, Robbert Krebbers, Herman Geuvers

FreeTensor: A Free-form DSL with Holistic Optimizations for Irregular Tensor Programs

Shizhi Tang, Jidong Zhai, Haojie Wang, Lin Jiang, Liyan Zheng, Zhenhao Yuan, Chen Zhang

2:00

Islaris: Verification of Machine Code Against Authoritative ISA Semantics

Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell

Lasagne: A Static Binary Translator for Weak Memory Model Architectures

Rodrigo C. O. Rocha, Dennis Sprokholt, Martin Fink, Redha Gouicem, Tom Spink, Soham Chakraborty, Pramod Bhatotia

2:20

RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code

Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer

Distinguished Paper Award

Verifying Optimizations of Concurrent Programs in the Promising Semantics

Junpeng Zha, Hongjin Liang, Xinyu Feng

2:40

3:00

3:20

Relational Compilation for Performance-Critical Applications

Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, Adam Chlipala

Interpreter-guided Differential JIT Compiler Unit Testing

Guillermo Polito, Stéphane Ducasse, Pablo Tesone

3:40

Formally Verified Lifting of C-compiled x86-64 Binaries

Freek Verbeek, Joshua A. Bockenek, Zhoulai Fu, Binoy Ravindran

Landmarks and Regions: A Robust Approach to Data Extraction

Suresh Parthasarathy, Lincy Pattanaik, Anirudh Khatry, Arun Iyer, Arjun Radhakrishna, Sriram Rajamani, Mohammad Raza

4:00

Leapfrog: Certified Equivalence for Protocol Parsers

Ryan Doenges, Tobias Kappé, John Sarracino, Nate Foster, Greg Morrisett

Odin: On-Demand Instrumentation with On-the-Fly Recompilation

Mingzhe Wang, Jie Liang, Chijin Zhou, Zhiyong Wu, Xinyi Xu, Yu Jiang

4:20

Computing Correctly with Inductive Relations

Zoe Paraskevopoulou, Aaron Eline, Leonidas Lampropoulos

Quickstrom: Property-based acceptance testing with LTL specifications

Liam O'Connor, Oskar Wickström

4:40