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 DanielssonLast updated Tue May 18 21:22:59 UTC 2010. |