Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: Stephan Swiderski <swiderski <at> informatik.rwth-aachen.de>
Subject: ANN: Haskell98 termination analyzer (AProVE)
Newsgroups: gmane.comp.lang.haskell.general
Date: Friday 8th September 2006 14:22:11 UTC (over 11 years ago)
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/
 
CD: 54ms