[Haskell] ANN: Haskell98 termination analyzer (AProVE)

[Stephan Swiderski]

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:
aprove at i2.informatik.rwth-aachen.de

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/