Hi Romain, are you aware of Haskabelle [1], a Haskell to Isabelle/HOL converter? I've never used or investigated it.

On 25.10.2010, at 10:09, Romain Demeyer wrote:

...

Hello,

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

Thanks,

-- Jean [1] http://isabelle.in.tum.de/haskabelle.html

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

Haskell functions may be verified interactively and/or automatically with Expander2 (http://fldit-www.cs.uni-dortmund.de/~peter/Expander2.html ). Induction, coinduction, narrowing and extendable sets of simplification rules admit proofs and computations at various levels of automation. All derivations are recorded both in textual form and in terms of straight-line programs that allow their stepwise replay. Peter Padawitz http://fldit-www.cs.tu-dortmund.de