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

This program is tentative and subject to change.

Thu 27 Jun 2024 10:40 - 11:00 at Finland / Norway - Formally Verified

Algorithms on restructuring binary search trees are typically presented in imperative pseudocode. Understandably so, as their performance relies on in-place execution, rather than the repeated allocation of fresh nodes in memory. Unfortunately, these imperative algorithms are notoriously difficult to verify as their loop invariants must relate the unfinished tree fragments being rebalanced.

This paper presents several novel functional algorithms for accessing and inserting elements in a restructuring binary search tree that are as fast as their imperative counterparts.

Yet the correctness of these functional algorithms is established using a simple inductive argument. For each data structure, move-to-root, splay, and zip trees, this paper describes both a bottom-up algorithm using zippers and a top-down algorithm using a novel first-class constructor context primitive. The functional and imperative algorithms are equivalent: we mechanise the proofs establishing this in the Coq proof assistant using the Iris framework. This yields a first fully verified implementation of well known algorithms on binary search trees with performance on par with the fastest implementations in C.

This program is tentative and subject to change.

Thu 27 Jun

Displayed time zone: Windhoek change

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 Pre-print
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 Pre-print
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