[Haskell] ANN: Haskell98 termination analyzer (AProVE)

Stephan Swiderski swiderski at informatik.rwth-aachen.de
Fri Sep 8 10:22:11 EDT 2006

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].

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.

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].

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].

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:
[2] web interface:
[3] RTA06 paper:
[4] experimental evaluation:

More information about the Haskell mailing list