Haskell

From Openproofs

Some approaches of proving programs implemented Haskell are:

• Translating subsets of Haskell to Isabelle, and verifying them.
• Using model checkers to verify subsets
• Extracting Haskell from Agda or Coq.

Some resources include:

• Graham Hutton's "Programming in Haskell" has a chapter on reasoning about Haskell code
• Tim Newsham's exercises of some short proofs for small Haskell functions
• Tim Newsham's 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.
• Tim Newsham's 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. More about this can be found in the Coq'Art book (as a good reference), 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/

(Much of this information comes from a Tim Newsham's 2009-02-03 posting "Re: [Haskell-cafe] Verifying Haskell Programs" on the Haskell-cafe mailing list. Thank you!)