Skip to Main content Skip to Navigation
Conference papers

Inductive types in the Calculus of Algebraic Constructions

Abstract : In a previous work, we proved that almost all of the Calculus of Inductive Constructions (CIC), which is the basis of the proof assistant Coq, can be seen as a Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. In this paper, we not only prove that CIC as a whole can be seen as a CAC, but also that it can be extended with non-free constructors, pattern-matching on defined symbols, non-strictly positive types and inductive-recursive types.
Document type :
Conference papers
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/inria-00105617
Contributor : Frédéric Blanqui <>
Submitted on : Wednesday, October 11, 2006 - 4:26:22 PM
Last modification on : Thursday, March 5, 2020 - 6:18:52 PM
Long-term archiving on: : Tuesday, April 6, 2010 - 7:24:37 PM

Files

Identifiers

Collections

Citation

Frédéric Blanqui. Inductive types in the Calculus of Algebraic Constructions. Typed Lambda Calculi and Applications, 6th International Conference, TLCA 2003, Jun 2003, Valencia, Spain. ⟨inria-00105617⟩

Share

Metrics

Record views

177

Files downloads

367