[Haskell] Specification and prover for Haskell

[Gerwin Klein]

On 25/10/2010, at 7:09 PM, Romain Demeyer wrote:
> I'm working on static verification in Haskell, and I search for existing works on specification of Haskell programs (such as pre/post conditions, for example) or any other functional language.

We have used Haskell extensively in the verification of the seL4 microkernel. One part of that was translating a prototype of the kernel into Isabelle and proving a large number of invariants as well as proving two refinement theorems about the translation. For our work the translation itself was not correctness critical, so we were happy to use our own somewhat ad-hoc tool for it.

Some papers on this are:

Pre/post verification and refinement of state monad programs:
http://www.cse.unsw.edu.au/~kleing/papers/Cock_KS_08.html

Experience report on the Haskell verification:
http://www.cse.unsw.edu.au/~kleing/papers/Klein_DE_09.html

The whole picture:
http://www.cse.unsw.edu.au/~kleing/papers/sosp09.html

More papers here: 
http://www.ertos.nicta.com.au/research/l4.verified/pubs.pml

In general, if your program does not use state monads, but is just a simple, straightforward functional program, the combination of Haskabelle and Isabelle/HOL can work quite nicely without a big formal apparatus such as a pre/post calculus. You can just state properties directly as you might in quickcheck.


> It would be great if there exists a prover based on this kind of specifications. I already found the ESC/Haskell. Do you know some other works which could be interesting?

We're using Isabelle/HOL. In the work above this was together with our own translator from Haskell to Isabelle, in the future it will possibly Haskabelle which has already been pointed out.

Cheers,
Gerwin