Skip to Main content Skip to Navigation
Reports

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

https://hal.inria.fr/inria-00099930
Contributor : Publications Loria <>
Submitted on : Wednesday, October 11, 2006 - 11:47:20 AM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Monday, April 5, 2010 - 11:52:27 PM

Identifiers

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

Share

Metrics

Record views

150

Files downloads

61