[Haskell-cafe] Proving correctness

Simon Thompson s.j.thompson at kent.ac.uk
Wed Feb 16 12:08:59 CET 2011

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]

Formulating Haskell [from Functional Programming, Glasgow 1992]

Miranda in Isabelle (with Steve Hill) [from Isabelle Workshop, 1995]


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

More information about the Haskell-Cafe mailing list