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

Full description

Bibliographic Details
Main Author: Hongwei Xi
Other Authors: The Pennsylvania State University CiteSeerX Archives
Format: Text
Language:English
Published: IEEE Computer Society Press 2001
Subjects:
DML
Online Access:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.69.9858
http://www.cs.bu.edu/~hwxi/academic/papers/HOSCdmlterm.pdf
id ftciteseerx:oai:CiteSeerX.psu:10.1.1.69.9858
record_format openpolar
spelling ftciteseerx:oai:CiteSeerX.psu:10.1.1.69.9858 2023-05-15T16:01:56+02:00 Dependent types for program termination verification Hongwei Xi The Pennsylvania State University CiteSeerX Archives 2001 application/pdf http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.69.9858 http://www.cs.bu.edu/~hwxi/academic/papers/HOSCdmlterm.pdf en eng IEEE Computer Society Press http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.69.9858 http://www.cs.bu.edu/~hwxi/academic/papers/HOSCdmlterm.pdf Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://www.cs.bu.edu/~hwxi/academic/papers/HOSCdmlterm.pdf text 2001 ftciteseerx 2016-01-08T18:21:20Z 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 2001
url http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.69.9858
http://www.cs.bu.edu/~hwxi/academic/papers/HOSCdmlterm.pdf
genre DML
genre_facet DML
op_source http://www.cs.bu.edu/~hwxi/academic/papers/HOSCdmlterm.pdf
op_relation http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.69.9858
http://www.cs.bu.edu/~hwxi/academic/papers/HOSCdmlterm.pdf
op_rights Metadata may be used without restrictions as long as the oai identifier remains attached to it.
_version_ 1766397611216994304