On Tue, Feb 3, 2009 at 12:28 AM, Don Stewart <d...@galois.com> wrote: > dbueno: >> 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!) > > > 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
