Titles in Development

Functional Data Structures and Algorithms: A Proof Assistant Approach

Author(s): Tobias Nipkow et al.
(Collection III)

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. The unique feature of this book is that all the proofs have been machine- checked by the proof assistant Isabelle. That is, in addition to the text in the book, which requires no knowledge of proof assistants, there are the Isabelle definitions and proofs that can be accessed by following (in the PDF file) the links attached to section headings with a symbol. The structured nature of Isabelle proofs permits even novices to browse them and follow the high-level arguments. This book has been classroom-tested for a number of years in a course for graduate and advanced undergraduate students. At the same time it is a reference for programmers and researchers who are interested in the details of some algorithm or proof.

< Back to Titles in Development List

---