Termination analysis with types is more accurate

Vitaly Lagoon; Fred Mesnard; Peter J. Stuckey

doi:10.1007/978-3-540-24599-5_18

Termination analysis with types is more accurate

Vitaly Lagoon, Fred Mesnard, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

12 Citations (Scopus)

Abstract

In this paper we show how we can use size and groundness analyses lifted to regular and (polymorphic) Hindley/Milner typed programs to determine more accurate termination of (type correct) programs. Type information for programs may be either inferred automatically or declared by the programmer. The analysis of the typed logic programs is able to completely reuse a framework for termination analysis of untyped logic programs by using abstract compilation of the type abstraction. We show that our typed termination analysis is uniformly more accurate than untyped termination analysis for regularly typed programs, and demonstrate how it is able to prove termination of programs which the untyped analysis can not.

Original language	English
Title of host publication	Logic Programming
Subtitle of host publication	19th International Conference, ICLP 2003 Mumbai, India, December 9-13, 2003 Proceedings
Editors	Catuscia Palamidessi
Place of Publication	Berlin Germany
Publisher	Springer
Pages	254-268
Number of pages	15
ISBN (Print)	3540206426
DOIs	https://doi.org/10.1007/978-3-540-24599-5_18
Publication status	Published - 1 Dec 2003
Externally published	Yes
Event	International Conference on Logic Programming 2003 - Mumbai, India Duration: 9 Dec 2003 → 13 Dec 2003 Conference number: ICLP 2003 https://link.springer.com/book/10.1007/b94619 (Proceedings)

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2916
ISSN (Print)	0302-9743

Conference

Conference	International Conference on Logic Programming 2003
Abbreviated title	ICLP 2003
Country/Territory	India
City	Mumbai
Period	9/12/03 → 13/12/03
Internet address	https://link.springer.com/book/10.1007/b94619 (Proceedings)

Access to Document

10.1007/978-3-540-24599-5_18

Cite this

@inproceedings{7742e3257c64499cafbb510461a61c7c,

title = "Termination analysis with types is more accurate",

abstract = "In this paper we show how we can use size and groundness analyses lifted to regular and (polymorphic) Hindley/Milner typed programs to determine more accurate termination of (type correct) programs. Type information for programs may be either inferred automatically or declared by the programmer. The analysis of the typed logic programs is able to completely reuse a framework for termination analysis of untyped logic programs by using abstract compilation of the type abstraction. We show that our typed termination analysis is uniformly more accurate than untyped termination analysis for regularly typed programs, and demonstrate how it is able to prove termination of programs which the untyped analysis can not.",

author = "Vitaly Lagoon and Fred Mesnard and Stuckey, \{Peter J.\}",

year = "2003",

month = dec,

day = "1",

doi = "10.1007/978-3-540-24599-5\_18",

language = "English",

isbn = "3540206426",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "254--268",

editor = "Catuscia Palamidessi",

booktitle = "Logic Programming",

address = "Switzerland",

note = "International Conference on Logic Programming 2003, ICLP 2003 ; Conference date: 09-12-2003 Through 13-12-2003",

url = "https://link.springer.com/book/10.1007/b94619",

}

Lagoon, V, Mesnard, F & Stuckey, PJ 2003, Termination analysis with types is more accurate. in C Palamidessi (ed.), Logic Programming: 19th International Conference, ICLP 2003 Mumbai, India, December 9-13, 2003 Proceedings. Lecture Notes in Computer Science, vol. 2916, Springer, Berlin Germany, pp. 254-268, International Conference on Logic Programming 2003, Mumbai, India, 9/12/03. https://doi.org/10.1007/978-3-540-24599-5_18

Termination analysis with types is more accurate. / Lagoon, Vitaly; Mesnard, Fred; Stuckey, Peter J.
Logic Programming: 19th International Conference, ICLP 2003 Mumbai, India, December 9-13, 2003 Proceedings. ed. / Catuscia Palamidessi. Berlin Germany: Springer, 2003. p. 254-268 (Lecture Notes in Computer Science; Vol. 2916).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

TY - GEN

T1 - Termination analysis with types is more accurate

AU - Lagoon, Vitaly

AU - Mesnard, Fred

AU - Stuckey, Peter J.

N1 - Conference code: ICLP 2003

PY - 2003/12/1

Y1 - 2003/12/1

N2 - In this paper we show how we can use size and groundness analyses lifted to regular and (polymorphic) Hindley/Milner typed programs to determine more accurate termination of (type correct) programs. Type information for programs may be either inferred automatically or declared by the programmer. The analysis of the typed logic programs is able to completely reuse a framework for termination analysis of untyped logic programs by using abstract compilation of the type abstraction. We show that our typed termination analysis is uniformly more accurate than untyped termination analysis for regularly typed programs, and demonstrate how it is able to prove termination of programs which the untyped analysis can not.

AB - In this paper we show how we can use size and groundness analyses lifted to regular and (polymorphic) Hindley/Milner typed programs to determine more accurate termination of (type correct) programs. Type information for programs may be either inferred automatically or declared by the programmer. The analysis of the typed logic programs is able to completely reuse a framework for termination analysis of untyped logic programs by using abstract compilation of the type abstraction. We show that our typed termination analysis is uniformly more accurate than untyped termination analysis for regularly typed programs, and demonstrate how it is able to prove termination of programs which the untyped analysis can not.

UR - http://www.scopus.com/inward/record.url?scp=0346895317&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-24599-5_18

DO - 10.1007/978-3-540-24599-5_18

M3 - Conference Paper

AN - SCOPUS:0346895317

SN - 3540206426

T3 - Lecture Notes in Computer Science

SP - 254

EP - 268

BT - Logic Programming

A2 - Palamidessi, Catuscia

PB - Springer

CY - Berlin Germany

T2 - International Conference on Logic Programming 2003

Y2 - 9 December 2003 through 13 December 2003

ER -

Termination analysis with types is more accurate

Abstract

Publication series

Conference

Access to Document

Other files and links

Cite this