Day 1: motivations, definitions and challenges

• Handout for day 1A: motivations and definitions (foldable version ; slides)
• Handout for day 1B: non-termination – aka: accidentally encoding the untyped lambda-calculus (foldable version ; slides)

Day 2: computability, and the higher-order recursive path ordering

• Handout for day 2: the higher-order recursive path ordreing (foldable version ; slides)

Day 3: static dependency pairs

• Handout for day 3: modular termination proofs using dependency pairs (foldable version ; slides)

Day 4: monotonic algebras as a method for termination and complexity

• Handout for day 4: tuple interpretations (foldable version ; slides)