|
Hongwei Xi
Dependent types for program termination
verification
Journal of Higher-Order and Symbolic Computation, 15:91-131,
October 2002
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.
[ bib |
.ps |
.pdf ]
Back
This file has been generated by
bibtex2html 1.61
Copyright notice: The documents contained
in these pages are included by the contributing authors as a means to
ensure timely dissemination of scholarly and technical work on a
non-commercial basis. Copyright and all rights therein are maintained
by the authors or by other copyright holders, notwithstanding that
they have offered their works here electronically. It is understood that all persons copying this information will
adhere to the terms and constraints invoked by each author's
copyright. These works
may not be reposted without the explicit permission of the copyright
holder.
If you experience problems downloading any of the files above,
it is most likely because your browser does not handle compressed
files correctly.
In particular, Netscape might save the file in the compressed
gz-format with extension .ps or
.pdf (indicating postscript or PDF, resp.). You can work around this by saving the file,
renaming it to .ps.gz or .pdf.gz, and then
uncrompress it.
|
