Specification and Verification of a Formal System for Structurally Recursive Functions

@inproceedings{abel99, abstract = {A type theoretic programming language is introduced that is based on lambda calculus with coproducts, products and inductive types, and additionally allows the definition of recursive functions in the way that is common in most functional programming languages. A formal system is presented that checks whether such a definition is structurally recursive and a soundness theorem is shown for this system. Thus all functions passing this check are ensured to terminate on all inputs. For the moment...}, author = {Abel, Andreas }, booktitle = {TYPES}, citeulike-article-id = {2877773}, keywords = {programming-languages, termination, type-theory}, pages = {1--20}, posted-at = {2008-06-09 18:51:52}, priority = {0}, title = {Specification and Verification of a Formal System for Structurally Recursive Functions}, url = {http://citeseer.ist.psu.edu/abel00specification.html}, year = {1999} }

TY - CONF ID - abel99 L3 - citeulike-article-id:2877773 TI - Specification and Verification of a Formal System for Structurally Recursive Functions T2 - TYPES SP - 1 EP - 20 N2 - A type theoretic programming language is introduced that is based on lambda calculus with coproducts, products and inductive types, and additionally allows the definition of recursive functions in the way that is common in most functional programming languages. A formal system is presented that checks whether such a definition is structurally recursive and a soundness theorem is shown for this system. Thus all functions passing this check are ensured to terminate on all inputs. For the moment... KW - programming-languages KW - termination KW - type-theory AU - Abel, Andreas PY - 1999/// UR - http://citeseer.ist.psu.edu/abel00specification.html ER -