On Mon, Feb 2, 2009 at 15:04, Don Stewart <d...@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!)
Denis
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
