I'd like to thank those folks who responded to my request for an Isabelle like system in Haskell. Whilst no one was able to point me to exactly what I was looking for, I did get helpful pointers to: http://www.cs.kun.nl/~janz/yarrow/ http://www.cs.yale.edu/homes/cc392/report.html http://www.math.chalmers.se/~rjmh/QuickCheck/ Brian