Un régime au concentré d'automate

Pierre-Marie Pédrot 1, 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Résumé : On présente dans cet article une optimisation a posteriori du format de fichier utilisé par l'assistant à la preuve Coq pour sauvegarder ses bibliothèques. L'implémentation purement fonctionnelle des structures de données contenues dans ces fichiers permet d'utiliser des algorithmes standards sur les automates qui garantissent de fait une optimalité du partage de la mémoire. Notre outil peut se généraliser directement au calcul du partage maximal lors de la sérialisation de toute structure de données OCaml utilisée de manière purement fonctionnelle.
Type de document :
Communication dans un congrès
Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs, Feb 2013, Aussois, France. 2013
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00779752
Contributeur : Ist Inria Saclay <>
Soumis le : mardi 22 janvier 2013 - 15:27:23
Dernière modification le : jeudi 15 novembre 2018 - 20:27:28
Document(s) archivé(s) le : samedi 1 avril 2017 - 08:21:56

Fichier

jfla2013-10.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : hal-00779752, version 1

Collections

Citation

Pierre-Marie Pédrot. Un régime au concentré d'automate. Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs, Feb 2013, Aussois, France. 2013. 〈hal-00779752〉

Partager

Métriques

Consultations de la notice

591

Téléchargements de fichiers

239