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" behaviour. chariot comes with a totality checker that tags such bad 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 due to L. Santocanale, - an interpretation of definitions as strategies for those games, - the Lee, Jones and Ben Amram's size-change principle, used to check that those strategies are "total". 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. It gives a practical argument in favor of this principle.

翻译：本文介绍了一种名为chariot的、具有嵌套归纳与共归纳代数数据类型的ML/Haskell风格编程语言。函数通过任意递归定义来定义，因此可能导致非终止及其他"不良"行为。chariot配备了一个完全性检查器，用于标记此类不良定义。在基于类型理论的证明助手（如Agda）中，这种完全性检查器是必不可少的。验证该检查器的正确性远非易事，其依赖于——L. Santocanale提出的将类型解释为对局博弈的方法，——将定义解释为这些博弈的策略，——以及Lee、Jones和Ben Amram的"规模变化原则"（用于检查这些策略是否"完全"）。本文着重阐述前两个要点，最后一步将是后续论文的研究主题。目前已经实现了一个原型系统，可用于实验性地检验该完全性检查器，这为该原则提供了实践支撑。