The Coq mailing list

[Sylvie Boldo <sylvie.boldo AT inria.fr>]

(English version below)

Le projet ANR FOST recrute pour 6 mois un postdoctorant sur le site de l'INRIA 
Saclay - Île-de-France à Orsay pour un début dès que possible.
Le projet FOST  cherche à vérifier formellement des programmes d'analyse 
numérique. Nous avons notamment réussi à prouver formellement la correction d'un 
schéma de résolution de l'équation des ondes 1D en utilisant l'assistant de 
preuves Coq. Le sujet proposé est la généralisation en dimension quelconque de 
cette preuve.
Une bonne connaissance de Coq ou d'un système similaire est souhaitée.

Voir http://fost.saclay.inria.fr et http://hal.inria.fr/inria-00450789/en/ 
(publié à ITP'10) pour plus de détails.


----

The FOST ANR projet seeks candidates for a postdoctoral positionfor 6 months at 
the INRIA Saclay - Île-de-France in Orsay, to begin as soon as possible.
The FOST projet aims at formally proving numerical analysis programs. In 
particular, we have formally proved the correctness of a numerical scheme that 
solves the 1D acoustic wave equation using the Coq proof assistant.
This postdoctoral work will generalize the proof to higher dimensions.
Extensive experience with Coq or similar provers is desirable.

See http://fost.saclay.inria.fr and http://hal.inria.fr/inria-00450789/en/ 
(published at ITP'10) for more details.


--
Sylvie Boldo, projet ProVal, INRIA Saclay - Île-de-France
Parc Orsay Université - 4 rue Jacques Monod - 91893 ORSAY Cedex