[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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 [EMAIL PROTECTED] Nicolas Magaud [EMAIL PROTECTED] Applications should be directed to {dufourd,[EMAIL PROTECTED] . Your application should contain a resume and a cover letter as well as references (e.g. your Master's thesis advisor). -- Nicolas Magaud mailto:[EMAIL PROTECTED] 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