[TYPES/announce] 10/12 months post-doc position in CerPAN project
Micaela Mayero
Micaela.Mayero at lipn.univ-paris13.fr
Wed Oct 17 11:24:52 EDT 2007
[Apologies for cross-posting]
==============================
Recrutement d'un post-doc dans le projet CerPAN
Post-doc position within the CerPAN project
** (English version follows) **
Le projet CerPAN est financé par l'ANR.
L'objectif de ce projet est de développer et mettre en application des
méthodes permettant de démontrer formellement la correction de programmes
issus du domaine de l'analyse numérique, en particulier sur les aspets
liés au calcul flottant et aux erreurs de méthode du schéma numérique.
Plus de détails sont disponibles sur la page du projet:
http://www-lipn.univ-paris13.fr/CerPAN/
Le projet recrute un post-doctorant sur le sujet suivant:
Développement de tactiques Coq dédiées aux nombres flottants (et réels)
ainsi que le développement d'une tactique Gappa (interface avec Why).
Début: à partir de novembre ou décembre 2007.
Durée: 10 à 12 mois.
Lieu: LIPN (équipe LCR, Université Paris 13) et LRI (projet ProVal,
Université Paris 11)
Contact: Micaela Mayero <Micaela.Mayero at lipn.univ-paris13.fr>
Sites en rapport avec le projet et le sujet:
http://www-lipn.univ-paris13.fr/LCR/
http://proval.lri.fr/presentation.fr.html
http://coq.inria.fr/coq-fra.html
http://why.lri.fr/index.fr.html
http://why.lri.fr/caduceus/index.en.html
http://lipforge.ens-lyon.fr/www/gappa/
http://www-lipn.univ-paris13.fr/CerPAN/
-------------------------------------------------------------
Post-doc position within the CerPAN project
The CerPAN project is financed by the "Agence Nationale de
la Recherche".
This project aims at developing and applying methods which allow us to
formally prove the soundness of programs from numerical analysis, in
particular aspects dealing with floating-point numbers and numerical
schema method errors.
More details are available on the web page:
http://www-lipn.univ-paris13.fr/CerPAN/?lang=english
The project recruits a post-doc on the following subject:
Development of Coq tactics dedicated to floating-point numbers (and real
numbers) and development of Gappa tactic (interfacing Why).
Starting date: as soon as possible from november 2007.
Duration: 10 to 12 months.
Place: LIPN (équipe LCR, Université Paris 13) et LRI (projet ProVal,
Université Paris 11)
eContact: Micaela Mayero <Micaela.Mayero at lipn.univ-paris13.fr>
Links:
http://www-lipn.univ-paris13.fr/LCR/?lang=uk
http://proval.lri.fr/presentation.en.html
http://coq.inria.fr/coq-eng.html
http://why.lri.fr/index.en.html
http://why.lri.fr/caduceus/index.en.html
http://lipforge.ens-lyon.fr/www/gappa/
http://www-lipn.univ-paris13.fr/CerPAN/?lang=english
More information about the Types-announce
mailing list