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.
Type de document :
Communication dans un congrès
TPHOLs (Emerging trends), Aug 2009, Munich, Germany. 2009, 〈http://tphols.in.tum.de/emerging-trends-TUM-I0916.pdf〉
Liste complète des métadonnées

Littérature citée [8 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00432649
Contributeur : Bruno Bernardo <>
Soumis le : lundi 16 novembre 2009 - 18:28:13
Dernière modification le : jeudi 11 janvier 2018 - 06:19:44
Document(s) archivé(s) le : jeudi 17 juin 2010 - 18:44:22

Fichier

bernardo-emerging-trends-tphol...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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), Aug 2009, Munich, Germany. 2009, 〈http://tphols.in.tum.de/emerging-trends-TUM-I0916.pdf〉. 〈inria-00432649〉

Partager

Métriques

Consultations de la notice

130

Téléchargements de fichiers

49