inria-00338974, version 1
Décurryfication certifiée
Journées Francophones des Langages Applicatifs (JFLA 2007) (2007) 119-134
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.
- 1 : GALLIUM (INRIA Rocquencourt)
- INRIA
- Domaine : Informatique/Langage de programmation
- inria-00338974, version 1
- http://hal.inria.fr/inria-00338974
- oai:hal.inria.fr:inria-00338974
- Contributeur : Xavier Leroy
- Soumis le : Vendredi 14 Novembre 2008, 19:05:52
- Dernière modification le : Samedi 15 Novembre 2008, 13:48:35
Documents associés
Exporter