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.

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. Naively using the size-change principle to check productivity and termination is straightforward but unsound when inductive and coinductive types are nested. We can however adapt the size-change principle to check ``totality'', which corresponds exactly to correctness with respect to the corresponding (co)inductive type.

We describe a way to represent computable functions between coinductive types as particular transducers in type theory. This generalizes earlier work on functions between streams by P. Hancock to a much richer class of coinductive types. Those transducers can be defined in dependent type theory without any notion of equality but require inductive-recursive definitions. Most of the properties of these constructions only rely on a mild notion of equality (intensional equality) and can thus be formalized in the dependently typed language Agda.

We present a categorical model for intuitionistic linear logic in which objects are polynomial diagrams and morphisms aresimulation diagrams. The multiplicative structure (tensor product and its adjoint) can be defined in any locally cartesian closed category, but the additive (product and coproduct) and exponential ( -comonoid comonad) structures require additional properties and are only developed in the categorySet, where the objects and morphisms have natural interpretations in terms of games, simulation and strategies.