Chapter 8: Termination Checking

In this chapter we discuss approaches to checking termination of functions defined by recursion on inductive data, both in type theory and strong functional programming.