Décurryfication certifiée

Zaynah Dargaye 1, *
* Auteur correspondant
Résumé : La décurryfication (transformation de fonctions curryfiées en fonctions n-aires) est une optimisation courante dans la compilation de langage fonctionnel. Nous présentons ici une preuve de préservation sémantique de cette optimisation menée dans l'assistant de preuve Coq.
Type de document :
Communication dans un congrès
Pierre-Etienne Moreau et Sandrine Blazy. Journées Francophones des Langages Applicatifs (JFLA 2007), Jan 2007, Aix-les-Bains, France. INRIA, pp.119-134, 2007


https://hal.inria.fr/inria-00338974
Contributeur : Xavier Leroy <>
Soumis le : vendredi 14 novembre 2008 - 19:05:52
Dernière modification le : lundi 5 octobre 2015 - 16:56:41
Document(s) archivé(s) le : mardi 9 octobre 2012 - 15:26:52

Fichier

dargaye.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00338974, version 1

Collections

Citation

Zaynah Dargaye. Décurryfication certifiée. Pierre-Etienne Moreau et Sandrine Blazy. Journées Francophones des Langages Applicatifs (JFLA 2007), Jan 2007, Aix-les-Bains, France. INRIA, pp.119-134, 2007. <inria-00338974>

Partager

Métriques

Consultations de
la notice

198

Téléchargements du document

81