[Haskell-cafe] Verifying Haskell Programs

Don Stewart dons at galois.com
Mon Feb 2 17:04:35 EST 2009

> Hi all,
> Much is talked that Haskell, since it is purely functional is easier >
to be verified.  > However, most of the research I have seen in software
verification > (either through model checking or theorem proving)
targets C/C++ or > subsets of these. What's the state of the art of
automatically > verifying properties of programs written in Haskell?

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

More information about the Haskell-Cafe mailing list