janvier  2006  –  Journées  Francophones  des  Langages  Applicatifs–  JFLA06

Table des matières

Arithmétique réelle exacte certifiée, co-induction et base arbitraire 1 Définition et preuve d’un algorithme fonctionnel de segmentation d’image basé sur

les hypercartes 15 Utilisation en Coq de l’opérateur de description 30 Les modèles classiques de conception objet

vus par la programmation ML 45 Couverture de code Caml pour la réalisation d’outils de développement certifiés 61 Un programme annoté en vaut deux 76 Erasure and Duplication in Classical Computation 91 Décurryfication certifiée 106 Union-Find Persistant 121 Gestion de versions de formats avec Camlp4 137

janvier  2006  –  Journées  Francophones  des  Langages  Applicatifs–  JFLA06

iv