Automated termination proofs for Haskell by term rewriting

J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, R. Thiemann

Research output: Contribution to journalArticleAcademicpeer-review

43 Citations (Scopus)
3 Downloads (Pure)

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.
Original languageEnglish
Article number7
Pages (from-to)7-1/39
Number of pages39
JournalACM Transactions on Programming Languages and Systems
Volume33
Issue number2
DOIs
Publication statusPublished - 2011

Fingerprint Dive into the research topics of 'Automated termination proofs for Haskell by term rewriting'. Together they form a unique fingerprint.

  • Cite this

    Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., & Thiemann, R. (2011). Automated termination proofs for Haskell by term rewriting. ACM Transactions on Programming Languages and Systems, 33(2), 7-1/39. [7]. https://doi.org/10.1145/1890028.1890030