This book is an introduction to data structures and algorithms for functional programming languages, with a focus on proofs. Starting with sorting and searching, it moves on to priority queues and advanced design and analysis techniques: dynamic programming, amortized analysis, splay trees, skew heaps and pairing heaps. The final part of the book covers a number of selected fun topics: graph algorithms, string search, Huffman’s algorithm for generating optimal codes, and alpha-beta pruning of game trees.

The book covers both correctness (does the algorithm do what it s supposed to do?) and running time analysis (does the algorithm terminate within a specified number of steps?). It does so in a unified anner with inductive proofs about functional programs and their running time functions.

What sets this book apart from existing books on algorithms is that all proofs have been machine-checked by the proof assistant Isabelle. In addition to the descriptions in the book, which require no knowledge of proof assistants, the Isabelle definitions and proofs are available online. The structured nature of Isabelle proofs permits even novices to follow the high-level arguments.

This book is aimed at teachers and students (it has been classroomtested for a number of years) but is also a reference work for programmers and researchers who are interested in the (verified!) details of some algorithm or proof.

Tobias Nipkow (born 1958) is a German computer scientist.
Career
Nipkow received his Diplom (MSc) in computer science from the Department of Computer Science of the Technische Hochschule Darmstadt in 1982, and his Ph.D. from the University of Manchester in 1987.
He worked at MIT from 1987, changed to Cambridge University in 1989, and to Technical University Munich in 1992, where he was appointed professor for programming theory.
He is chair of the Logic and Verification group since 2011.
He is known for his work in interactive and automatic theorem proving, in particular for the Isabelle proof assistant; he was the editor of the Journal of Automated Reasoning up to January 1, 2021. Moreover, he focuses on programming language semantics, type systems and functional programming.
In 2021 he won the Herbrand Award "in recognition of his leadership in developing Isabelle and related tools, resulting in key contributions to the foundations, automation, and use of proof assistants in a wide range of applications, as well as his successful efforts in increasing the visibility of automated reasoning".
In 2022, he was elected a member of the Academia Europaea.