Structural recursive definitions in type theory

Abstract

We introduce an extension of the Calculus of Construction with inductive and co-inductive types that preserves normalisation, while keeping a relatively simple collection of typing rules. This extension considerably enlarges the expressiveness of the language, enabling a direct representation of recursive programs in type theory.