https://fdsa-book.net/

Functional Data Structures and Algorithms

A Proof Assistant Approach

Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Alejandro
Gomez-Londono, 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:

Functional Data Structures and Algorithms

Table of contents 1 Table of contents 2

This book is meant to evolve over time. If you would like to
contribute, get in touch!