Advertisement
Published in:
2006 | OriginalPaper | Chapter
CIC: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
Authors : Gilles Barthe, Benjamin Grégoire, Fernando Pastawski
Published in: Logic for Programming, Artificial Intelligence, and Reasoning
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Sized types provides a type-based mechanism to enforce termination of recursive definitions in typed
λ
-calculi. Previous work has provided strong indications that type-based termination provides an appropriate foundation for proof assistants based on type theory; however, most work to date has been confined to non-dependent type systems. In this article, we introduce a variant of the Calculus of Inductive Constructions with sized types and study its meta theoretical properties: subject reduction, normalization, and thus consistency and decidability of type-checking and of size-inference. A prototype implementation has been developed alongside case studies.