Title: First Steps Towards Cumulative Inductive Types in CIC
Authors: Timany, Amin
Jacobs, Bart
Issue Date: 2015
Publisher: Springer International Publishing
Host Document: Theoretical Aspects of Computing - ICTAC 2015 vol:9399 pages:608-617
Series Title: Lecture Notes in Computer Science
Conference: Theoretical Aspects of Computing - ICTAC 2015 edition:12 location:Cali, Colombia date:29-31 October 2015
Abstract: Having the type of all types in a type system results in paradoxes like Russel’s paradox. Therefore type theories like predicative calculus of inductive constructions (pCIC) - the logic of the Coq proof assistant - have a hierarchy of types Type0, Type1, Type2, . . . , where Type0 : Type1, Type1 : Type2, . . . . In a cumulative type system, e.g., pCIC, for a term t such that t: Type i we also have that t: Typei + 1. The system pCIC has recently been extended to support universe polymorphism, i.e., definitions can be parametrized by universe levels. This extension does not support cumulativity for inductive types. For example, we do not have that a pair of types at levels i and j is also considered a pair of types at levels i + 1 and j + 1.
In this paper, we discuss our on-going research on making inductive types cumulative in the pCIC. Having inductive types be cumulative alleviates some problems that occur while working with large inductive types, e.g., the category of small categories, in pCIC.
We present the pCuIC system which adds cumulativity for inductive types to pCIC and briefly discuss some of its properties and possible extensions. We, in addition, give a justification for the introduced cumulativity relation for inductive types.
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
CIT.pdf Published 344KbAdobe PDFView/Open
PCuIC.pdf Published 416KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science