HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 Connect in order to contact the contributor
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

57

Files downloads

144