[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:
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/
More information about the Haskell-Cafe
mailing list