  This paper introduces an ML / Haskell like programming language with nested
inductive and coinductive algebraic datatypes called chariot. Functions are
defined by arbitrary recursive definitions and can thus lead to non-termination
and other "bad" behavior. chariot comes with a //totality checker// that tags
possibly ill-behaved definitions. Such a totality checker is mandatory in the
context of proof assistants based on type theory like Agda.Proving correctness
of this checker is far from trivial and relies on - an interpretation of types
as parity games, - an interpretation of correct values as winning strategies
for those games, - the Lee, Jones and Ben Amram's size-change principle, used
to check that the strategies induced by recursive definitions are winning.This
paper develops the first two points, the last step being the subject of an
upcoming paper.A prototype has been implemented and can be used to experiment
with the resulting totality checker, giving a practical argument in favor of
this principle.
