An evidence supporting approach
Tobias Nipkow, Jasmine Blanchett, Manuel Eberal, Alejandro Gomez-Londoña, Peter Lammich, Christian Sterngel, Simon Wimmer, Baohua Zhan
Published by ACM Books
This book is an introduction to data structures and algorithms for functional languages, with a focus on proofs. This includes both functional correctness and running time analysis. It does this in a unified manner with inductive proofs about functions of functional programs and their running times. All the evidence has been machine checked by proof assistant Isabel. The PDF contains links to related Isabelle principles.
Click on an image to download a PDF of the full book:
This book is meant to evolve over time. If you’d like to contribute, get in touch!
<a href