Functional Data Structures and Algorithms

A Proof Assistant Approach

Tobias Nipkow, Mohammad Abdulaziz, Jasmin Blanchette, Manuel Eberl, Alejandro Gómez-Londoño, Peter Lammich, Lawrence Paulson, 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 verification. 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.

An early version of the book was available online as Functional Algorithms, Verified!

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!