Many termination checkers support lexicographic (structural) recursion.  The lexicographic combination of orderings on sets A and B is an ordering on A x B where a pair decreases if the A component does (and then the B component can increase unboundedly) or else the A component stays the same and the B component decreases.  Connections with nested recursion and ordinals discussed.

Another type-based approach to termination-checking for recursive functions over inductive datatypes is to use so-called Mendler-style iteration.  On this approach, we write recursive functions by coding against a certain interface that features an abstract type R, which abstracts the datatype over which we are recursing; and a function from R to the result type of the recursion.  Subdata of the input data are available at type R only, not at the original datatype.  This allows us to make explicit recursive calls, but only on subdata.

Well-founded recursion is a technique to turn recursion which decreases along a well-founded ordering into a structural recursion.

Discussion of a compositional method of termination checking using so-called sized types.  Datatypes are indexed by sizes, and recursive calls can only be made on data of strictly smaller size than the data as input to the recursion.  Since the method is type-based, it is compositional: we can break out helper functions from a recursive function and not upset the termination checker.  A readable and interesting tutorial on the subject is here.

Review of need for termination analysis for recursive functions on inductive datatypes.  Discussion of a serious problem with syntactic termination checks, namely noncompositionality.  A function may pass the syntactic termination check, but abstracting part of it out into a helper function may result in code which no longer passes the check.  So we need a compositional termination check, which will be discussed in subsequent episodes.

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.  

Discussion of the basic idea of the Tait--Martin-Loef proof of confluence for untyped lambda calculus.  Let me know any requests for what to discuss in Chapter 8!

Start of discussion on how to prove confluence for untyped lambda calculus.  Also some discussion about the research community interested in confluence.

The basic property of confluence of a nondeterministic reduction semantics: if from starting term t you can reach t1 and also t2 (by two finite reduction sequences), then there is some t3 to which t1 and t2 both reduce in a finite number of steps.  The use of confluence for ensuring completeness of the conversion-checking algorithm that tests conversion of t1 and t2 by normalizing both terms and checking for alpha-equivalence (or maybe alpha,eta-equivalence).

Discussion of the connection between normalization and logical consistency.  One approach is to prove normalization and type preservation, to show (in proof-theoretic terms) that all detours can be eliminated from proofs (this is normalization) and that the resulting proof still proves the same theorem (this is type preservation).  I mention an alternative I use for Cedille, which is to use a realizability semantics (often used for normalization proofs) directly to prove consistency.