A Predicative Analysis of Structural Recursion Export

@unpublished{abel02, abstract = {. We introduce a language based upon lambda calculus with products, coproducts and strictly positive inductive types that allows the denition of recursive terms. We present the implementation (\foetus\") of a syntactical check that ensures that all such terms are structurally recursive, i.e. recursive calls appear only with arguments structurally smaller than the input parameters of considered terms. To ensure the correctness of the termination checker, we show that all structurally recursive...}, author = {Abel, Andreas and Altenkrich, Thorsten}, citeulike-article-id = {2877767}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.6971}, keywords = {programming-languages, termination}, posted-at = {2008-06-09 18:50:07}, priority = {0}, title = {A Predicative Analysis of Structural Recursion}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.6971}, year = {1999} }

TY - UNPB ID - abel02 L3 - citeulike-article-id:2877767 N2 - . We introduce a language based upon lambda calculus with products, coproducts and strictly positive inductive types that allows the denition of recursive terms. We present the implementation (\foetus") of a syntactical check that ensures that all such terms are structurally recursive, i.e. recursive calls appear only with arguments structurally smaller than the input parameters of considered terms. To ensure the correctness of the termination checker, we show that all structurally recursive... TI - A Predicative Analysis of Structural Recursion KW - programming-languages KW - termination AU - Abel, Andreas AU - Altenkrich, Thorsten PY - 1999/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.6971 ER -