[Haskell-cafe] Verifying Haskell Programs
thomas.dubuisson at gmail.com
Sun Feb 1 09:24:41 EST 2009
On Sun, Feb 1, 2009 at 12:54 PM, Paulo J. Matos <pocmatos at gmail.com> wrote:
> What's the state of the art of automatically
> verifying properties of programs written in Haskell?
This is a large field that isn't as black and white as many people
frame it. You can write a proof  then translate that into Haskell,
you can write Haskell then prove key functions, using a case totality
checker you could prove it doesn't have any partial functions that
will cause an abnormal exit , some research has been performed into
information flow at UPenn , and SPJ/Zu have been looking at static
contract checking  for some time now - which I hope sees the light
of day in GHC 6.12. While this work has been going on, folks at
Portland State and a few others (such as Andy Gill , NICTA , and
Peng Li to an extent) have been applying FP to the systems world 
Hope this helps,
 Perhaps using Isabelle, isabelle.in.tum.de.
 Neil built CATCH for just this purpose (though it isn't in GHC
 Strongly typed memory areas, http://web.cecs.pdx.edu/~mpj/pubs/bytedata.html
 Some work on non-inference as well as thoughts on building a
 Timber language - no, I haven't looked at it yet myself.
More information about the Haskell-Cafe