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!