[Haskell-cafe] Verifying Haskell Programs

[Tim Newsham]

>> 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:
   http://www.cs.nott.ac.uk/~gmh/book.html

I put together some exercises of some short proofs for small
Haskell functions:
   http://www.thenewsh.com/~newsham/formal/problems/

I have a short article that covers proofs in Haskell and Isabelle:
   http://users.lava.net/~newsham/formal/reverse/

The seL4 project is specifying an OS in Haskell, proving it in Isabelle
and translating it to C with proofs that connect the translations:
   http://ertos.nicta.com.au/research/sel4/

I have an article on the curry-howard correspondence
   http://www.thenewsh.com/~newsham/formal/curryhoward/

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:
   http://www.labri.fr/perso/casteran/CoqArt/index.html
   http://www.cs.harvard.edu/~adamc/cpdt/
   http://www.cs.harvard.edu/~adamc/cpdt/book/
   http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/

>                              Denis

Tim Newsham
http://www.thenewsh.com/~newsham/