[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
[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 <[EMAIL PROTECTED]> 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 <[EMAIL PROTECTED]> 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