Sciweavers

Share
LISP
2002

Dependent Types for Program Termination Verification

9 years 9 months ago
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 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 ...
Hongwei Xi
Added 22 Dec 2010
Updated 22 Dec 2010
Type Journal
Year 2002
Where LISP
Authors Hongwei Xi
Comments (0)
books