Harnessing First Order Termination Provers Using Higher Order Dependency Pairs

C. Fuhs; C.L.M. Kop

doi:10.1007/978-3-642-24364-6_11

Harnessing First Order Termination Provers Using Higher Order Dependency Pairs

C. Fuhs, C.L.M. Kop

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

Many functional programs and higher order term rewrite systems contain, besides higher order rules, also a significant first order part. We discuss how an automatic termination prover can split a rewrite system into a first order and a higher order part. The results are applicable to all common styles of higher order rewriting with simple types, although some dependency pair approach is needed to use them. © 2011 Springer-Verlag.

Original language	English
Pages (from-to)	147-162
Journal	Lecture Notes in Computer Science
Volume	6989
DOIs	https://doi.org/10.1007/978-3-642-24364-6_11
Publication status	Published - 2011
Event	Frontiers of Combining Systems - Duration: 1 Jan 2011 → 1 Jan 2011

Bibliographical note

Proceedings title: Proc. 8th Symposium on Frontiers of Combining Systems - FroCoS'11
Publisher: Springer
ISBN: 978-3-642-24363-9
Editors: C. Tinelli, V. Sofronie-Stokkermans

Access to Document

10.1007/978-3-642-24364-6_11

http://www.springerlink.com/content/b035j4920671k101/export-citation/

Persistent URL (handle)

Persistent link

Cite this

@article{dcf1acac53d24a2cbd7ac22997667915,

title = "Harnessing First Order Termination Provers Using Higher Order Dependency Pairs",

abstract = "Many functional programs and higher order term rewrite systems contain, besides higher order rules, also a significant first order part. We discuss how an automatic termination prover can split a rewrite system into a first order and a higher order part. The results are applicable to all common styles of higher order rewriting with simple types, although some dependency pair approach is needed to use them. {\textcopyright} 2011 Springer-Verlag.",

author = "C. Fuhs and C.L.M. Kop",

note = "Proceedings title: Proc. 8th Symposium on Frontiers of Combining Systems - FroCoS'11 Publisher: Springer ISBN: 978-3-642-24363-9 Editors: C. Tinelli, V. Sofronie-Stokkermans; Frontiers of Combining Systems ; Conference date: 01-01-2011 Through 01-01-2011",

year = "2011",

doi = "10.1007/978-3-642-24364-6_11",

language = "English",

volume = "6989",

pages = "147--162",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Springer Science and Business Media Deutschland GmbH",

}

TY - JOUR

T1 - Harnessing First Order Termination Provers Using Higher Order Dependency Pairs

AU - Fuhs, C.

AU - Kop, C.L.M.

N1 - Proceedings title: Proc. 8th Symposium on Frontiers of Combining Systems - FroCoS'11 Publisher: Springer ISBN: 978-3-642-24363-9 Editors: C. Tinelli, V. Sofronie-Stokkermans

PY - 2011

Y1 - 2011

N2 - Many functional programs and higher order term rewrite systems contain, besides higher order rules, also a significant first order part. We discuss how an automatic termination prover can split a rewrite system into a first order and a higher order part. The results are applicable to all common styles of higher order rewriting with simple types, although some dependency pair approach is needed to use them. © 2011 Springer-Verlag.

AB - Many functional programs and higher order term rewrite systems contain, besides higher order rules, also a significant first order part. We discuss how an automatic termination prover can split a rewrite system into a first order and a higher order part. The results are applicable to all common styles of higher order rewriting with simple types, although some dependency pair approach is needed to use them. © 2011 Springer-Verlag.

U2 - 10.1007/978-3-642-24364-6_11

DO - 10.1007/978-3-642-24364-6_11

M3 - Article

SN - 0302-9743

VL - 6989

SP - 147

EP - 162

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

T2 - Frontiers of Combining Systems

Y2 - 1 January 2011 through 1 January 2011

ER -

Harnessing First Order Termination Provers Using Higher Order Dependency Pairs

Abstract

Bibliographical note

Access to Document

Persistent URL (handle)

Fingerprint

Cite this