Changements de représentation des données dans le calcul des constructions inductives

Nicolas Magaud 1 Yves Bertot 1
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Résumé : Dans le calcul des constructions inductives, des outils de calcul et de preuve sont associés à chaque type de données concret défini inductivement. Par conséquent, le choix d'une structure de données influence fortement le contenu des preuves. Nous proposons dans ce document une méthode pour passer plus facilement d'une structure de données à une autre, en effectuant des traductions partiellement automatisées des preuves. Un prototype d'outil de traduction a été développé dans le système Coq et a été expérimenté sur des traductions de preuves de l'arithmétique de Peano vers l'arithmétique binaire.
Type de document :
Rapport
[Rapport de recherche] RR-4039, INRIA. 2000, pp.29
Liste complète des métadonnées

https://hal.inria.fr/inria-00072599
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 10:22:05
Dernière modification le : samedi 27 janvier 2018 - 01:30:58
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:14:55

Fichiers

Identifiants

  • HAL Id : inria-00072599, version 1

Collections

Citation

Nicolas Magaud, Yves Bertot. Changements de représentation des données dans le calcul des constructions inductives. [Rapport de recherche] RR-4039, INRIA. 2000, pp.29. 〈inria-00072599〉

Partager

Métriques

Consultations de la notice

73

Téléchargements de fichiers

212