Haskell functions may be verified interactively and/or automatically
with Expander2 (http://fldit-www.cs.uni-dortmund.de/~peter/Expander2.html
).
Induction, coinduction, narrowing and extendable sets of
simplification rules admit proofs and computations at various levels
of automation.
All derivations are recorded both in textual form and in terms of
straight-line programs that allow their stepwise replay.
Peter Padawitz
http://fldit-www.cs.tu-dortmund.de
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
