BROADCASTS.com

b'

Start of Chapter 8 of the podcast, on termination checking in type theory, and strong functional programming.\\xa0 Discussion of a little history of adding datatypes to the original pure type theory of Coq (called the Calculus of Constructions).\\xa0 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.\\xa0\\xa0