Coq à la conquête des moulins

Laurence Rideau 1 Bernard Serpette 2
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
2 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Résumé : Nous presentons la certification formelle en Coq d'un algorithme utilise' dans les compilateurs: l'affectation parallele de registres. Nous proposons deux specifications inductives et une specification fonctionnelle de l'algorithme ainsi que les preuves de correction de ces specifications. Un code fonctionnel ML peut etre extrait de la specification fonctionnelle et integre' au code du compilateur.
Liste complète des métadonnées

https://hal.inria.fr/inria-00001128
Contributor : Laurence Rideau <>
Submitted on : Tuesday, February 21, 2006 - 4:52:09 PM
Last modification on : Monday, November 5, 2018 - 3:36:03 PM
Document(s) archivé(s) le : Saturday, April 3, 2010 - 8:08:45 PM

Identifiers

  • HAL Id : inria-00001128, version 1

Collections

Citation

Laurence Rideau, Bernard Serpette. Coq à la conquête des moulins. Olivier Michel. JFLA '2005, Mar 2005, Obernai, INRIA, pp.169-180, 2005, JFLA 2005 : actes de la conférence journées francophones des langages applicatifs. 〈inria-00001128〉

Share

Metrics

Record views

277

Files downloads

162