Fortune's algorithm is a sweep line algorithm to construct the Voronoi diagram of a set of points in the plane. Voronoi diagrams have applications in many domains of activities, for instance concerning antenna placement and robot motion planning. In this task, we wish to develop a formal description of Voronoi diagrams and of the algorithm proposed by Steven Fortune in 1986, in the context of the Coq system and the mathematical components library. If time allows, we also wish to study how executable algorithms can be derived from the formal description.

The intern will have to work with the Coq system. Documentation for the various aspects of the work can be obtained in the following manner:

- General documentation about Coq: the Coq web site
- A general purpose book on Coq:
*Interactive Theorem Proving and Program development; Coq'Art: the calculus of inductive constructions, (Springer) 2004, ISBN 3-540-20854-2*(internet site, Version française) - The mathematical components library: the mathematical components web site, The book on mathematical components.