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.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00072599
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:22:05 AM
Last modification on : Monday, September 3, 2018 - 10:56:02 AM
Long-term archiving on: Sunday, April 4, 2010 - 11:14:55 PM

Identifiers

  • 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⟩

Share

Metrics

Record views

92

Files downloads

232