Termination of rewriting and its certification

A. Koprowski

Research output: ThesisPhd Thesis 1 (Research TU/e / Graduation TU/e)Academic

Abstract

In programming, termination of a program/algorithm means that its evaluation will eventually terminate, regardless of the input it receives. It is an important property and is required for total correctness. In general the problem is undecid- able. Term rewriting is a formal way of specifying computation and as such it can be seen as a generic model for programming languages. Termination, here meaning lack of infinite sequences, is a well-studied concept in this context. There exist a number of methods for proving termination as well as a number of tools for doing that automatically. There is an on-going work on application of this methodology and tools to proving termination of programs in actual programming languages. In this thesis we first give a short introduction to term rewriting and to termination of rewriting. Subsequently we present a number of contributions to this field, which can be categorized into the following categories: proposing new methods for proving termination and refining the existing ones, developing a tool for proving termination and proposing a methodology and tools for certification of termination proofs, i.e., formal verification of proofs produced by the existing tools for proving termination.
LanguageEnglish
QualificationDoctor of Philosophy
Awarding Institution
  • Department of Mathematics and Computer Science
Supervisors/Advisors
  • Zantema, Hans, Promotor
  • Groote, Jan Friso, Promotor
Award date25 Sep 2008
Place of PublicationEindhoven
Publisher
Print ISBNs978-90-386-1377-2
DOIs
StatePublished - 2008

Fingerprint

Computer programming languages
Refining
Formal verification

Cite this

Koprowski, A. (2008). Termination of rewriting and its certification Eindhoven: Technische Universiteit Eindhoven DOI: 10.6100/IR637480
Koprowski, A.. / Termination of rewriting and its certification. Eindhoven : Technische Universiteit Eindhoven, 2008. 186 p.
@phdthesis{82d28df2888b4ece982e49d936a79ccc,
title = "Termination of rewriting and its certification",
abstract = "In programming, termination of a program/algorithm means that its evaluation will eventually terminate, regardless of the input it receives. It is an important property and is required for total correctness. In general the problem is undecid- able. Term rewriting is a formal way of specifying computation and as such it can be seen as a generic model for programming languages. Termination, here meaning lack of infinite sequences, is a well-studied concept in this context. There exist a number of methods for proving termination as well as a number of tools for doing that automatically. There is an on-going work on application of this methodology and tools to proving termination of programs in actual programming languages. In this thesis we first give a short introduction to term rewriting and to termination of rewriting. Subsequently we present a number of contributions to this field, which can be categorized into the following categories: proposing new methods for proving termination and refining the existing ones, developing a tool for proving termination and proposing a methodology and tools for certification of termination proofs, i.e., formal verification of proofs produced by the existing tools for proving termination.",
author = "A. Koprowski",
year = "2008",
doi = "10.6100/IR637480",
language = "English",
isbn = "978-90-386-1377-2",
publisher = "Technische Universiteit Eindhoven",
school = "Department of Mathematics and Computer Science",

}

Koprowski, A 2008, 'Termination of rewriting and its certification', Doctor of Philosophy, Department of Mathematics and Computer Science, Eindhoven. DOI: 10.6100/IR637480

Termination of rewriting and its certification. / Koprowski, A.

Eindhoven : Technische Universiteit Eindhoven, 2008. 186 p.

Research output: ThesisPhd Thesis 1 (Research TU/e / Graduation TU/e)Academic

TY - THES

T1 - Termination of rewriting and its certification

AU - Koprowski,A.

PY - 2008

Y1 - 2008

N2 - In programming, termination of a program/algorithm means that its evaluation will eventually terminate, regardless of the input it receives. It is an important property and is required for total correctness. In general the problem is undecid- able. Term rewriting is a formal way of specifying computation and as such it can be seen as a generic model for programming languages. Termination, here meaning lack of infinite sequences, is a well-studied concept in this context. There exist a number of methods for proving termination as well as a number of tools for doing that automatically. There is an on-going work on application of this methodology and tools to proving termination of programs in actual programming languages. In this thesis we first give a short introduction to term rewriting and to termination of rewriting. Subsequently we present a number of contributions to this field, which can be categorized into the following categories: proposing new methods for proving termination and refining the existing ones, developing a tool for proving termination and proposing a methodology and tools for certification of termination proofs, i.e., formal verification of proofs produced by the existing tools for proving termination.

AB - In programming, termination of a program/algorithm means that its evaluation will eventually terminate, regardless of the input it receives. It is an important property and is required for total correctness. In general the problem is undecid- able. Term rewriting is a formal way of specifying computation and as such it can be seen as a generic model for programming languages. Termination, here meaning lack of infinite sequences, is a well-studied concept in this context. There exist a number of methods for proving termination as well as a number of tools for doing that automatically. There is an on-going work on application of this methodology and tools to proving termination of programs in actual programming languages. In this thesis we first give a short introduction to term rewriting and to termination of rewriting. Subsequently we present a number of contributions to this field, which can be categorized into the following categories: proposing new methods for proving termination and refining the existing ones, developing a tool for proving termination and proposing a methodology and tools for certification of termination proofs, i.e., formal verification of proofs produced by the existing tools for proving termination.

U2 - 10.6100/IR637480

DO - 10.6100/IR637480

M3 - Phd Thesis 1 (Research TU/e / Graduation TU/e)

SN - 978-90-386-1377-2

PB - Technische Universiteit Eindhoven

CY - Eindhoven

ER -

Koprowski A. Termination of rewriting and its certification. Eindhoven: Technische Universiteit Eindhoven, 2008. 186 p. Available from, DOI: 10.6100/IR637480