Automated Termination Proofs for Haskell by Term Rewriting
Jürgen Giesl, Matthias Raffelsieper, Peter Schneider-Kamp, Stephan Swiderski, and René ThiemannACM Transactions on Programming Languages and Systems 33(2), 2011.
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"
}
© ACM (2011). This is the author’s version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM TOPLAS, 33(2):7, 2011, http://doi.acm.org/10.1145/1890028.1890030.