Re: [Haskell-cafe] Verifying Haskell Programs

On Mon, Feb 2, 2009 at 10:04 PM, Don Stewart wrote:

pocmatos:

...

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.

Any references to publications related to this?

-- Don

-- Paulo Jorge Matos - pocmatos at gmail.com Webpage: http://www.personal.soton.ac.uk/pocm