The Size-Change Principle for Mixed Inductive and Coinductive types

This paper shows how to use Lee, Jones and Ben Amram's size-change principle to check correctness of arbitrary recursive definitions in an ML / Haskell like programming language with inductive and coinductive types. The size-change principle is used to check both termination and productivity, and the resulting principle is sound even if inductive and coinductive types are arbitrarily nested. A prototype has been implemented and gives a practical argument in favor of this principle. This work relies on a characterization of least and greatest fixed points as sets of winning strategies for parity games that was developed by L. Santocanale in his early work on circular proofs. The proof of correctness of the criterion relies on an extension of the language's denotational semantics to a domain of untyped values with non-deterministic sums.