[Haskell-cafe] Verifying Haskell Programs

[Don Stewart]

dbueno:
> On Mon, Feb 2, 2009 at 15:04, Don Stewart <dons at galois.com> 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.
> 
> 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?
> 
> (It's not that I don't believe you -- I'd be really interested to read it!)


All on haskell.org,

    http://haskell.org/haskellwiki/Research_papers/Testing_and_correctness#Verifying_Haskell_programs

And there's been work since I put that list together.

-- Don