Dans des travaux précédents, nous avons donné des descriptions formelles abstraites d'algorithmes de calculs d'enveloppe convexe en dimension 2. Les algorithmes ont été décrits par des programmes fonctionnels purs et la démonstration de correction de ces algorithmes a été complètement vérifiée mécaniquement, à l'aide du système de démonstration sur ordinateur Coq. Ces travaux ont donné lieu à une publication dans une conférence internationale (TPHOLs2001).
On cherche à pousser plus loin l'étude de ces algorithmes en allant dans deux directions.
D'une part, on cherche à obtenir des programmes impératifs certifiés, dans lesquels des considérations d'efficacités ont également été prises en compte. On pourra alors être amené à démontrer la correction de plusieurs optimisations sur les algorithmes.
D'autre part, on cherche à comprendre quelles sont les bonnes structures de données pour étendre les résultats obtenus à la troisième dimension. voir (http://www-sop.inria.fr/lemme/stages/geometrie.html)
David Pichardie and Yves Bertot,
"Formalizing Convex Hulls Algorithms"
,
Proceedings of TPHOLs'01, LNCS 2152, pp. 346-361.