[Haskell-cafe] Verifying Haskell Programs
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
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:
More information about the Haskell-Cafe