Start of Chapter 8 of the podcast, on termination checking in type theory, and strong functional programming.  Discussion of a little history of adding datatypes to the original pure type theory of Coq (called the Calculus of Constructions).  Considering the most basic form of termination checking, which is checking syntactically that recursive calls are only made on subdata of the data input to the recursive function.