Abstract
Type-based termination is a method to enforce termination of recursive definitions through a non-standard type system that introduces a notion of size for inhabitants of inductively defined types. The purpose of this tutorial is to provide a gentle introduction to a polymorphically typed λ-calculus with type-based termination, and to the size inference algorithm which is used to guarantee automatically termination of recursive definitions. © 2009 Springer Berlin Heidelberg.
Cite
CITATION STYLE
Barthe, G., Grégoire, B., & Riba, C. (2009). A tutorial on type-based termination. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5520 LNCS, pp. 100–152). https://doi.org/10.1007/978-3-642-03153-3_3
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
