[Haskell-cafe] Verifying Haskell Programs

Paulo J. Matos pocmatos at gmail.com
Tue Feb 3 03:31:00 EST 2009


On Mon, Feb 2, 2009 at 10:04 PM, 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.
>

Any references to publications related to this?

> -- Don
>



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


More information about the Haskell-Cafe mailing list