Lambda the Ultimate

inactiveTopic Isabelle/HOL: A Proof Assistant for Higher-Order Logic
started 4/11/2002; 2:50:57 AM - last post 4/11/2002; 6:55:41 AM
Ehud Lamm - Isabelle/HOL: A Proof Assistant for Higher-Order Logic  blueArrow
4/11/2002; 2:50:57 AM (reads: 1430, responses: 1)
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel. Isabelle/HOL -- A Proof Assistant for Higher-Order Logic. LNCS 2283.

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

Ehud Lamm - Re: Isabelle/HOL: A Proof Assistant for Higher-Order Logic  blueArrow
4/11/2002; 6:55:41 AM (reads: 651, responses: 0)
Obviously you can prove more complicated things using Isabelle. The last chapter of this well written tutorial shows the verfication of a complex security protocol.

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...