Sciweavers

Share
LPAR
2010
Springer

On Strong Normalization of the Calculus of Constructions with Type-Based Termination

8 years 3 months ago
On Strong Normalization of the Calculus of Constructions with Type-Based Termination
Termination of recursive functions is an important property in proof assistants based on dependent type theories; it implies consistency and decidability of type checking. Type-based termination is a mechanism for ensuring termination that uses types annotated with size information to check that recursive calls are performed on smaller arguments. Our long-term goal is to extend the Calculus of Inductive Constructions with a type-based termination mechanism and prove its logical consistency. In this paper, we present an extension of the Calculus of Constructions (including universes and impredicativity) with sized natural numbers, and prove strong normalization and logical consistency. Moreover, the proof can be easily adapted to include other inductive types.
Benjamin Grégoire, Jorge Luis Sacchini
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where LPAR
Authors Benjamin Grégoire, Jorge Luis Sacchini
Comments (0)
books