Type-based termination

Andreas Abel addresses the problem of ensuring that computer programs terminates, meaning that their execution halts after some time and delivers a result. He considers functional programs in which repeating computations are programmed with recursion. By the use of a type system, recursion is restricted to guarantee termination; only terminating programs, yet not all, are accepted by the compiler. Several classical algorithms from computer science textbooks are implemented in this language with the type-based termination check in order to demonstrate its expressivity and practicality. The type-based termination check is mathematically proven correct by constructing a semantics where each type is interpreted by a set of terminating programs. The book is aimed at researchers and professionals with a strong interest in programming language theory.