Machine-Checked Correctness and Complexity of a Union-Find Implementation

Union-Find is a famous example of a simple data structure whose amortized asymptotic time complexity analysis is non-trivial. Using Coq and the CFML tool, Arthur Charguéraud and I have verified the correctness and amortized complexity of an OCaml implementation of Union-Find. In this talk, I will give an overview of our approach, which uses higher-order separation logic extended with time credits. This approach allows us to state (and establish) a single specification that covers correctness and complexity at the same time.

Speaker Details

F. Pottier is a researcher at INRIA. He is known for his work on constraints-based type inference in ML; alpha-conversion; his work on GADTs and, more recently, for a series of heroic, Coq-based soundness proofs, including that of Mezzo, a new, permission-based dialect of ML that blends separation logic and type systems.

Date:
Speakers:
Francois Pottier
Affiliation:
INRIA

    • Portrait of Jeff Running

      Jeff Running