Linear Sized Types in the Calculus of Constructions

Sized types provide an expressive and compositional framework for proving termination and productivity of (co-) recursive definitions. In this paper, we study sized types with linear annotations of the form n . alpha + m with n and m natural numbers. Concretely, we present a type system with linear sized types for the Calculus of Constructions extended with one inductive type (natural numbers) and one coinductive type (streams). We show that this system satisfies desirable metatheoretical properties, including strong normalization, and give a sound and complete size-inference algorithm.