Book details

Functional Data Structures and Algorithms: A Proof Assistant Approach

by Tobias Nipkow , Jasmin Blanchette , Manuel Eberl , Alejandro Gómez-Londoño , Peter Lammich , Christian Sternagel , Simon Wimmer , Bohua Zhan

Categories Functional programming , Data structures , Algorithms , Theorem prover

This book develops functional data structures and algorithms with formal verification of both functional correctness and running time. It presents inductive proofs about programs and their cost functions, with every proof machine-checked in Isabelle and linked to the corresponding theories.