[Haskell-cafe] Verifying Haskell Programs

Tim Newsham newsham at lava.net
Tue Feb 3 10:54:01 EST 2009

>> State of the art is translating subsets of Haskell to Isabelle, and
>> verifying them. Using model checkers to verify subsets, or extracting
>> Haskell from Agda or Coq.
> Don, can you give some pointers to literature on this, if any?  That
> is, any documentation of a verification effort of Haskell code with
> Isabelle, model checkers, or Coq?

Graham Hutton's _Programming in Haskell_ has a chapter on reasoning
about Haskell code:

I put together some exercises of some short proofs for small
Haskell functions:

I have a short article that covers proofs in Haskell and Isabelle:

The seL4 project is specifying an OS in Haskell, proving it in Isabelle
and translating it to C with proofs that connect the translations:

I have an article on the curry-howard correspondence

In systems like Coq you can write code and proofs of the code in
the same language and even at the same time.  The Coq'Art book is
a good reference, as are Adam Chlipala's draft book and Harvard
class materials and the _Type Theory & Functional Programming_ book.
Full text for all but Coq'Art are online:

>                              Denis

Tim Newsham

More information about the Haskell-Cafe mailing list