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...
Other Authors: | |
---|---|
Format: | Text |
Language: | English |
Subjects: | |
Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.118.1930 http://www.cs.bu.edu/~hwxi/academic/papers/lics01.pdf |
id |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.118.1930 |
---|---|
record_format |
openpolar |
spelling |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.118.1930 2023-05-15T16:01:56+02:00 Dependent Types for Program Termination Verification ∗ The Pennsylvania State University CiteSeerX Archives application/pdf http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.118.1930 http://www.cs.bu.edu/~hwxi/academic/papers/lics01.pdf en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.118.1930 http://www.cs.bu.edu/~hwxi/academic/papers/lics01.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/lics01.pdf text ftciteseerx 2016-01-07T13:58:09Z 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 |
title |
Dependent Types for Program Termination Verification ∗ |
spellingShingle |
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 ∗ |
url |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.118.1930 http://www.cs.bu.edu/~hwxi/academic/papers/lics01.pdf |
genre |
DML |
genre_facet |
DML |
op_source |
http://www.cs.bu.edu/~hwxi/academic/papers/lics01.pdf |
op_relation |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.118.1930 http://www.cs.bu.edu/~hwxi/academic/papers/lics01.pdf |
op_rights |
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
_version_ |
1766397606050660352 |