[Haskell-cafe] Proving correctness
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?
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe