Skip to Main content Skip to Navigation
Conference papers

Towards an Implicit Calculus of Inductive Constructions. Extending the Implicit Calculus of Constructions with Union and Subset Types.

Abstract : We present extensions of Miquel's Implicit Calculus of Constructions (ICC) and Barras and Bernardo's decidable Implicit Calculus of Constructions (ICC*) with union and subset types. The purpose of these systems is to solve the problem of interaction betweeen logical and computational data. This is a work in progress and our long term goal is to add the whole inductive types to ICC and ICC* in order to define a complete framework for theorem proving.
Document type :
Conference papers
Complete list of metadata

Cited literature [8 references]  Display  Hide  Download

https://hal.inria.fr/inria-00432649
Contributor : Bruno Bernardo <>
Submitted on : Monday, November 16, 2009 - 6:28:13 PM
Last modification on : Thursday, March 5, 2020 - 6:21:58 PM
Long-term archiving on: : Thursday, June 17, 2010 - 6:44:22 PM

File

bernardo-emerging-trends-tphol...
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00432649, version 1

Collections

Citation

Bruno Bernardo. Towards an Implicit Calculus of Inductive Constructions. Extending the Implicit Calculus of Constructions with Union and Subset Types.. TPHOLs (Emerging trends), TU München, Aug 2009, Munich, Germany. ⟨inria-00432649⟩

Share