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@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
