Définition de la classe de réécriture à intégrer

Frédéric Blanqui 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Nous définissons les objets qui doivent être rajoutés à Coq pour pouvoir définir des fonctions à l'aide de règles de récriture, et décrivons les conditions qui doivent être vérifiées pour que la correction de Coq soit préservée. Cela constitue une sorte de ``cahier des charges'' pour le futur prototype.
Type de document :
Rapport
[Contrat] A04-R-487 || blanqui04c, 2004, 7 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00099930
Contributeur : Publications Loria <>
Soumis le : mercredi 11 octobre 2006 - 11:47:20
Dernière modification le : jeudi 8 février 2018 - 11:32:01
Document(s) archivé(s) le : lundi 5 avril 2010 - 23:52:27

Identifiants

  • HAL Id : inria-00099930, version 1

Collections

Citation

Frédéric Blanqui. Définition de la classe de réécriture à intégrer. [Contrat] A04-R-487 || blanqui04c, 2004, 7 p. 〈inria-00099930〉

Partager

Métriques

Consultations de la notice

117

Téléchargements de fichiers

43