Dear all, we are pleased to announce the integration of an
automatic Haskell98 termination analyzer in the termination tool AProVE [1]. Our tool accepts full Haskell as specified in the Haskell 98 Report and is available through our web interface [2]. USE Our tool checks termination of given start terms w.r.t. a Haskell program. A start term is a Haskell term accepted by the command line of Haskell interpreters like GHCi or Hugs. Moreover, start terms may contain free variables representing arbitrary terminating terms. EXAMPLE For example the start term "take x (repeat y)" can be proved terminating (where "take" and "repeat" are defined in the Haskell prelude). On the other hand, the start term "repeat y" does not terminate, because the function "repeat" generates the infinite list of "y"s. For more details on our approach see [3]. EXPERIMENTS We evaluated our tool on standard libraries (Prelude, List, ...) of the Hugs implementation. In this setting we could show the termination of almost 80 percent of 1281 start terms resulting from these libraries. More details on the evaluation can be found in [4]. FEEDBACK We would be grateful for comments and suggestions on our tool or on our approach. Please send them to: [EMAIL PROTECTED] Stephan Swiderski, Jürgen Giesl, Peter Schneider-Kamp, René Thiemann [1] AProVE home page: http://aprove.informatik.rwth-aachen.de [2] web interface: http://aprove.informatik.rwth-aachen.de/index.asp?subform=termination_proofs.html&program_type=hs [3] RTA06 paper: http://aprove.informatik.rwth-aachen.de/eval/Haskell/RTA06-distribute.ps [4] experimental evaluation: http://aprove.informatik.rwth-aachen.de/eval/Haskell/ _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
