Under consideration for publication in Math. Struct. in Comp. Science Type-based termination of recursive

The paper introduces λ ̂ , a simply typed lambda calculus supporting inductive types and recursive function definitions with termination ensured by types. The system is shown to enjoy subject reduction, strong normalization of typable terms and to be stronger than a related system λG in which termination is ensured by a syntactic guard condition. The system can, at will, be extended to also support coinductive types and corecursive function definitions. 1