[Haskell-cafe] Verifying Haskell Programs

[Paulo J. Matos]

On Tue, Feb 3, 2009 at 12:28 AM, Don Stewart <dons at galois.com> wrote:
> 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.
>

Opps, sorry, missed this message. Should read everything before replying! :)

> -- Don
>



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