Monday 13 May 2019, 10:30, LSV library: The size-change principle for mixed induction and coinduction, Pierre Hyvernat (LAMA).

The Size-Change Principle (SCP) is a simple algorithm giving a partial termination test for recursive definitions. If the language is lazy, it also gives (by duality) a partial productivity test for recursive functions involving coinductive types. This is what is used in Agda.
Unfortunately, when inductive and coinductive types are nested, this is unsound: there are "well typed" and terminating recursive definitions producing terms in empty types. Such definitions make Agda inconsistant.
Using ideas from L. Santocanale about circular proof and parity games, I'll show how the SCP can be used to check "totality" of recursive definitions. Besides the SCP, the main ingredient is a more informative of call-graph, and I'll sketch the proof of correctness by defining their semantics using power domains.