Changements de représentation des données dans le calcul des constructions inductives - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2000

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

Nicolas Magaud
Yves Bertot

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.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
RR-4039.pdf (334.45 Ko) Télécharger le fichier

Dates et versions

inria-00072599 , version 1 (24-05-2006)

Identifiants

  • HAL Id : inria-00072599 , version 1

Citer

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⟩
43 Consultations
164 Téléchargements

Partager

Gmail Facebook X LinkedIn More