[TYPES/announce] PhD position available : Building reliable programs in computational geometry and certifying them with Coq

[Nicolas Magaud]

A three-year PhD-student position is open at LSIIT 
(http://lsiit.u-strasbg.fr )
in the field of formal proofs in geometry. This proposal fits in the 
GALAPAGOS
research project which has been accepted by the french research agency 
(ANR) in 2007.

This thesis will be supervised by Professor Jean-François Dufourd and 
co-advised
by Nicolas Magaud (http://http://dpt-info.u-strasbg.fr/~jfd/ .

We would like it to start as soon as possible (at the end of 2007 at the 
latest).

Context :
---------
In the GALAPAGOS project, we wish to apply computerized theorem proving 
tools to two aspects
of geometry. The first aspect concerns computational geometry, the 
second step concerns verifying
geometric reasoning steps in usual constructions, such as constructions 
with ruler and compass.

Thesis proposal : Building reliable programs in computational geometry 
and certifying them
------------------------------------------------------------------------------------------
This thesis aims at improving software quality and at designing new 
algorithms in the field
of computational geometry. To achieve this goal, we shall use 
combinatorial maps as our
topological model and use formal methods to specify, interactively prove 
and automatically
extract programs from their proofs of correctness.
This work will be carried out in the Calculus of Inductive Constructions 
and implemented
via the Coq proof assistant. From a specification and a constructive 
proof, its enables us
to extract an Ocaml program via the proofs-as-programs paradigm. This, 
the program is
certified, meaning that it always terminates and that it satisfies its 
specification.
Geometric objects we shall consider are plane subdivisions, modeled by 
embedded combinatorial
maps. Embeddings will be linear and most combinatorial maps involved 
will be planar.
This thesis will make us revisit classic problems in computational 
geometry, among them,
handling plane subdivisions, computing convex hulls, performing point 
location, co-refining
maps, computing Delaunay and Voronoï diagrams. This should be sufficient 
to show our methodology
benefits, especially proof techniques for structural and/or noetherian 
induction on subdivisions.
This will allow us to deal with more complex algorithms such as those 
required in 3D.

Contact Information :
---------------------

For further information about this position, please contact either:

 Jean-François Dufourd     dufourd at dpt-info.u-strasbg.fr
 Nicolas Magaud            magaud at dpt-info.u-strasbg.fr


Applications should be directed to 
{dufourd,magaud}@dpt-info.u-strasbg.fr . Your application
should contain a resume and a cover letter as well as references (e.g. 
your Master's thesis advisor).

-- 
Nicolas Magaud                    mailto:magaud at dpt-info.u-strasbg.fr
LSIIT - UMR 7005 CNRS-ULP                    Tel: (+33) 3 90 24 45 61
Bd Sébastien Brant - BP 10413                Fax: (+33) 3 90 24 44 55
67412 ILLKIRCH CEDEX - FRANCE    http://dpt-info.u-strasbg.fr/~magaud