[Haskell-cafe] Proving correctness

[Simon Thompson]

I did some work years ago about giving a predicate logic treatment of Haskell, based on earlier work for Miranda, and formalised some proofs based on this in Isabelle. Here are the links:

Logic for Miranda, revisited [from Formal Aspects of Computing, 1995]
  http://www.cs.kent.ac.uk/pubs/1995/63/index.html

Formulating Haskell [from Functional Programming, Glasgow 1992]
  http://www.cs.kent.ac.uk/pubs/1992/123/index.html

Miranda in Isabelle (with Steve Hill) [from Isabelle Workshop, 1995]
  http://www.cs.kent.ac.uk/pubs/1995/209/index.html
  
Regards,

Simon




On 11 Feb 2011, at 11:06, C K Kashyap wrote:

> Hi Folks,
> 
> I've come across this a few times - "In Haskell, once can prove the correctness of the code" - Is this true?
> 
> I know that static typing and strong typing of Haskell eliminate a whole class of problems - is that related to the proving correctness?
> Is it about Quickcheck - if so, how is it different from having test sutites in projects using mainstream languages?
> 
> 
> Regards,
> Kashyap
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe