Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Alejandro Gómez-Londoño, Peter Lammich, Christian Sternagel, Simon Wimmer, Bohua Zhan

Published by ACM Books

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!