Quotients dans le CCI

Loïc Pottier 1
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Résumé : On étudie plusieurs voies pour formaliser les quotients dans le Calcul de Constructions Inductive: les quotients naïfs (en utilisant les travaux de [LW99] et [BB96],onmontre qu´ils conduisent à une incohérence), les quotients décidables, les quotients classiques de la théorie des types (comme ceux étudiés dans [Hof95], et finallement on propose une notion de quotients fonctionnels qui résolvent les problèmes des précédentes notions, et semblent satisfaisants théoriquement et pratiquement. Pour chaque notion introduite au cours du papier, on donne la traduction correspond- ante dans le système Coq [pro99].
Type de document :
Rapport
RR-4053, INRIA. 2000
Liste complète des métadonnées

https://hal.inria.fr/inria-00072584
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 10:20:31
Dernière modification le : jeudi 11 janvier 2018 - 16:24:45
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:14:23

Fichiers

Identifiants

  • HAL Id : inria-00072584, version 1

Collections

Citation

Loïc Pottier. Quotients dans le CCI. RR-4053, INRIA. 2000. 〈inria-00072584〉

Partager

Métriques

Consultations de la notice

156

Téléchargements de fichiers

109