A tutorial on type-based termination, in

Abstract. Type-based termination is a method to enforce termination of recursive definitions through a non-standard type system that intro-duces a notion of size for inhabitants of inductively defined types. The purpose of this tutorial is to provide a gentle introduction to a polymor-phically typed λ-calculus with type-based termination, and to the size inference algorithm which is used to guarantee automatically termination of recursive definitions.