Termination Checking in the Presence of Nested Inductive and Coinductive Types
Thorsten Altenkirch, Nils Anders Danielsson · EPiC series in computing · 2018
In 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.