Termination checking with types

@misc{citeulike:345254, abstract = {The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces   , a lambda-calculus with recursion, inductive types, subtyping and bounded quanti cation. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm...}, author = {Abel, A. }, citeulike-article-id = {345254}, keywords = {termination}, posted-at = {2008-04-15 15:01:39}, priority = {2}, title = {Termination checking with types}, url = {http://citeseer.ist.psu.edu/abel99termination.html}, year = {2002} }

TY - GEN ID - citeulike:345254 L3 - citeulike-article-id:345254 TI - Termination checking with types N2 - The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces   , a lambda-calculus with recursion, inductive types, subtyping and bounded quanti cation. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm... KW - termination AU - Abel, A PY - 2002/// UR - http://citeseer.ist.psu.edu/abel99termination.html ER -