<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
@inproceedings{XiLICS01,
author = "Hongwei Xi",
title = {{Dependent Types for Program Termination Verification}},
booktitle = "Proceedings of 16th IEEE Symposium on Logic in Computer Science",
year = 2001,
month = "June",
pages = "231--242",
address = "Boston",
abstract = {{
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.
}}
}