Functional Data Structures and Algorithms: a Proof Assistant Approach

Summary

Functional Data Structures and Algorithms A Proof Assistant Approach This book is an introduction to data structures and algorithms for functional languages, with a focus on proofs. It covers both functional correctness and running time analysis. It does so in a unified manner with inductive proofs about functional programs and their running time functions. All proofs have been machine-checked by the proof assistant Isabelle. The pdf contains links to the corresponding Isabelle theories. Click on an image to download the pdf of the whole book: This book is meant to evolve over time. If you would like to contribute, get in touch!