Abstract

There are many powerful techniques for automated termination analysis of
term rewriting. However, up to now they have hardly been used for real
programming languages. We present a new approach which permits the
application of existing techniques from term rewriting to prove termination
of most functions defined in Haskell programs. In particular, we show how
termination techniques for ordinary rewriting can be used to handle those
features of Haskell which are missing in term rewriting (e.g., lazy
evaluation, polymorphic types, and higher-order functions). We implemented
our results in the termination prover AProVE and successfully evaluated
them on existing Haskell libraries.

BibTeX

@article{JGMRPSKSSRT-TOPLAS11,
  author      = "J{\"u}rgen Giesl and Matthias Raffelsieper and
                 Peter Schneider-Kamp and Stephan Swiderski and
                 Ren{\'e} Thiemann",
  title       = "Automated Termination Proofs for {Haskell} by Term
                 Rewriting",
  journal     = "{ACM} Transactions on Programming Languages and Systems",
  volume      = 33,
  number      = 2,
  year        = 2011,
  ee          = "http://doi.acm.org/10.1145/1890028.1890030"
}