## Termination Checking in the Presence of Nested Inductive and Coinductive TypesTermination Checking in the Presence of Nested Inductive and Coinductive Types ## AbstractIn the dependently typed functional programming language Agda one can easily mix induction and coinduction. The implementation of the termination/productivity checker is based on a simple extension of a termination checker for a language with inductive types. However, this simplicity comes at a price: only types of the form νX.μY.F X Y can be handled directly, not types of the form μY.νX.F X Y. We explain the implementation of the termination checker and the ensuing problem. Nils Anders DanielssonDisclaimer Last updated Tue May 18 21:22:59 UTC 2010. |