Functional Data Structures and Algorithms. A Proof Assistant Approach

A Proof Assistant Approach

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!