The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

(Version Française en fin de message)
------------------------------------------------------------------------

INRIA (Sophia-Antipolis near Nice, France) is looking for :

*two young doctors in computer science for a short term working
contract of 4 months each *for instance as a relay position while
awaiting for a postdoctoral position (gross monthly salary : 2240 Euros per
month).

Under the supervision of Yves Bertot, head of and the Marelle team at
INRIA, you will contribute to the development of a web-based course on

*Safe functional programming with the coq system *

We hope to propose an exciting challenge at the frontiers of Web
technologies and computer based proving.

The task will consist in organizing the different elements of a
multimedia course, in implementing exercises from the material proposed
by researchers and teachers, and in developing game-like applications to
convey some notions of computer-based proof. Among other frameworks, the
scenarii approach supported by the unit numerical University will be
used for this project.

Please send a resume and a cover letter to 
*Yves.Bertot AT inria.fr*
<mailto:Yves.Bertot AT inria.fr>

Réferences :

* Yves' homepage http://www-sop.inria.fr/members/Yves.Bertot/
* safe functional programming with the coq system
http://fuscia.info/coq/
* the Marelle team at INRIA http://www-sop.inria.fr/marelle/
* the coq system http://coq.inria.fr/
* the existing exercises on the coq book site
http://www.labri.fr/perso/casteran/CoqArt/
* the fuscia project http://fuscia.info/
* UNIT numerical University on engineering and technology
http://www.unit.eu/
* INRIA http://www.inria.fr/

------------------------------------------------------------------------

L’INRIA (centre de Sophia-Antipolis Méditerrannée) recherche :

*deux jeunes docteurs sur CDD pour un travail de courte durée* de 4
mois environ chacun à partir de mai ou juin 2009 (rémunération 2240
euros brut mensuel ) par exemple en attendant le début d’un séjour
postdoctoral.

Leur travail consistera, sous la direction de Yves Bertot responsable de
l’équipe Marelle de l’Inria, à contribuer à la réalisation d’un cours
sur le web sur

*Programmation fonctionnelle sûre à l'aide du système Coq*.

C'est un défi excitant à l'interface entre les technologies Web et la
démonstration sur ordinateur.

Le travail consistera à organiser les différents éléments du cours
multi-média dans un ouvrage cohérent, à réaliser certains des exercices
à partir de matériel proposé par des chercheurs et enseignants, et à
développer des applications ludiques mettant en relief certains aspects
de la démonstration sur ordinateur. On utilisera notamment la
technologie scenarii soutenue par l'université thématique UNIT.

Cette offre est une opportunité de participer à une réalisation
novatrice en e-learning et de travailler quelques mois au sein d’un
Institut prestigieux comme l’Inria.

Adresser un CV et un courrier à 
*Yves.Bertot AT inria.fr
<mailto:Yves.Bertot AT inria.fr>*

Références :
* Cette page http://www-sop.inria.fr/members/Yves.Bertot/coqcdd09.html
* page d’Yves Bertot http://www-sop.inria.fr/members/Yves.Bertot/
* projet de cours Programmation fonctionnelle sûre à l'aide du
système Coq http://fuscia.info/coq/
* l’équipe Marelle de l’Inria http://www-sop.inria.fr/marelle/
* le système coq http://coq.inria.fr/
* les exercices existants sur le site coqArt
http://www.labri.fr/perso/casteran/CoqArt/
* le projet fuscia http://fuscia.info/
* UNIT Université numérique Ingénierie et technologie
http://www.unit.eu/
* l'INRIA http://www.inria.fr/

------------------------------------------------------------------------