Automated Termination Proofs for Haskell by Term Rewriting

Jürgen Giesl, Matthias Raffelsieper, Peter Schneider-Kamp, Stephan Swiderski, René Thiemann

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

Resumé

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.
OriginalsprogEngelsk
TidsskriftA C M Transactions on Programming Languages and Systems
Vol/bind33
Udgave nummer2
Sider (fra-til)Article 7
Antal sider39
ISSN0164-0925
DOI
StatusUdgivet - 2011

Fingeraftryk

Computer programming languages

Citer dette

Giesl, Jürgen ; Raffelsieper, Matthias ; Schneider-Kamp, Peter ; Swiderski, Stephan ; Thiemann, René. / Automated Termination Proofs for Haskell by Term Rewriting. I: A C M Transactions on Programming Languages and Systems. 2011 ; Bind 33, Nr. 2. s. Article 7.
@article{75a82bd74ec0416191d545acd5453178,
title = "Automated Termination Proofs for Haskell by Term Rewriting",
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.",
author = "J{\"u}rgen Giesl and Matthias Raffelsieper and Peter Schneider-Kamp and Stephan Swiderski and Ren{\'e} Thiemann",
year = "2011",
doi = "10.1145/1890028.1890030",
language = "English",
volume = "33",
pages = "Article 7",
journal = "A C M Transactions on Programming Languages and Systems",
issn = "0164-0925",
publisher = "Association for Computing Machinery",
number = "2",

}

Automated Termination Proofs for Haskell by Term Rewriting. / Giesl, Jürgen; Raffelsieper, Matthias; Schneider-Kamp, Peter; Swiderski, Stephan; Thiemann, René.

I: A C M Transactions on Programming Languages and Systems, Bind 33, Nr. 2, 2011, s. Article 7.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - Automated Termination Proofs for Haskell by Term Rewriting

AU - Giesl, Jürgen

AU - Raffelsieper, Matthias

AU - Schneider-Kamp, Peter

AU - Swiderski, Stephan

AU - Thiemann, René

PY - 2011

Y1 - 2011

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

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

U2 - 10.1145/1890028.1890030

DO - 10.1145/1890028.1890030

M3 - Journal article

VL - 33

SP - Article 7

JO - A C M Transactions on Programming Languages and Systems

JF - A C M Transactions on Programming Languages and Systems

SN - 0164-0925

IS - 2

ER -