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/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
