Dependent Types for Program Termination Verification
Program termination verification is a challenging research subject of significant practical importance. While there is already a rich body of literature on this subject, it is still undeniably a difficult task to design a termination checker for a realistic programming language that supports general...
Main Author: | |
---|---|
Other Authors: | |
Format: | Text |
Language: | English |
Published: |
IEEE Computer Society Press
2000
|
Subjects: | |
Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.8835 http://www.ececs.uc.edu/~hwxi/academic/papers/lics01.ps |
id |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.28.8835 |
---|---|
record_format |
openpolar |
spelling |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.28.8835 2023-05-15T16:01:57+02:00 Dependent Types for Program Termination Verification Hongwei Xi The Pennsylvania State University CiteSeerX Archives 2000 application/postscript http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.8835 http://www.ececs.uc.edu/~hwxi/academic/papers/lics01.ps en eng IEEE Computer Society Press http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.8835 http://www.ececs.uc.edu/~hwxi/academic/papers/lics01.ps Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://www.ececs.uc.edu/~hwxi/academic/papers/lics01.ps text 2000 ftciteseerx 2016-01-07T21:01:59Z Program termination verification is a challenging research subject of significant practical importance. While there is already a rich body of literature on this subject, it is still undeniably a difficult task to design a termination checker for a realistic programming language that supports general recursion. In this paper, we present an approach to program termination verification that makes use of a form of dependent types developed in Dependent ML (DML), demonstrating a novel application of such dependent types to establishing a liveness property. We design a type system that enables the programmer to supply metrics for verifying program termination and prove that every well-typed program in this type system is terminating. We also provide realistic examples, which are all verified in a prototype implementation, to support the effectiveness of our approach to program termination verification as well as its unobtrusiveness to programming. The main contribution of the paper lies in the design of an approach to program termination verification that smoothly combines types with metrics, yielding a type system capable of guaranteeing program termination that supports a general form of recursion (including mutual recursion), higher-order functions, algebraic datatypes, and polymorphism. 1 Text DML Unknown |
institution |
Open Polar |
collection |
Unknown |
op_collection_id |
ftciteseerx |
language |
English |
description |
Program termination verification is a challenging research subject of significant practical importance. While there is already a rich body of literature on this subject, it is still undeniably a difficult task to design a termination checker for a realistic programming language that supports general recursion. In this paper, we present an approach to program termination verification that makes use of a form of dependent types developed in Dependent ML (DML), demonstrating a novel application of such dependent types to establishing a liveness property. We design a type system that enables the programmer to supply metrics for verifying program termination and prove that every well-typed program in this type system is terminating. We also provide realistic examples, which are all verified in a prototype implementation, to support the effectiveness of our approach to program termination verification as well as its unobtrusiveness to programming. The main contribution of the paper lies in the design of an approach to program termination verification that smoothly combines types with metrics, yielding a type system capable of guaranteeing program termination that supports a general form of recursion (including mutual recursion), higher-order functions, algebraic datatypes, and polymorphism. 1 |
author2 |
The Pennsylvania State University CiteSeerX Archives |
format |
Text |
author |
Hongwei Xi |
spellingShingle |
Hongwei Xi Dependent Types for Program Termination Verification |
author_facet |
Hongwei Xi |
author_sort |
Hongwei Xi |
title |
Dependent Types for Program Termination Verification |
title_short |
Dependent Types for Program Termination Verification |
title_full |
Dependent Types for Program Termination Verification |
title_fullStr |
Dependent Types for Program Termination Verification |
title_full_unstemmed |
Dependent Types for Program Termination Verification |
title_sort |
dependent types for program termination verification |
publisher |
IEEE Computer Society Press |
publishDate |
2000 |
url |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.8835 http://www.ececs.uc.edu/~hwxi/academic/papers/lics01.ps |
genre |
DML |
genre_facet |
DML |
op_source |
http://www.ececs.uc.edu/~hwxi/academic/papers/lics01.ps |
op_relation |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.8835 http://www.ececs.uc.edu/~hwxi/academic/papers/lics01.ps |
op_rights |
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
_version_ |
1766397617695096832 |