This book is a self-contained introduction to interactive proof in higher-order logic (HOL), using the proof assistant Isabelle2002. It is a tutorial for potential users rather than a monograph for researchers.
It is quite exciting to see how familiar functional programming constructs can be used directly inside a theorem prover. But beware, HOL is not the same as Haskell:
As we have indicated, the requirement for total functions is an essential characteristic of HOL. It is only because of totality that reasoning in HOL is comparatively easy. More generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as function definitions whose totality has not been proved) because they quickly lead to inconsistencies. Instead, fixed constructs for introducing types and functions are offered (such as datatype and primrec) which are guaranteed to preserve consistency.
Still it is quite cool to see how much goes into proving that reverse(reverse(lst))=lst. For the detailed proof see chapter 2: Functional Programming in HOL.
Posted to Misc-Books by Ehud Lamm on 4/11/02; 3:57:52 AM
I gave my SE and Ada course students the task of coding and proving the correctness of a function merging two sorted vectors. I wish I could have made them use Isabelle...