The Coq mailing list

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

********************** Post-Doc Announcement **********************

The INRIA research action "Concert" proposes a post-doctoral research
grant for students interested and the formalization and certification
of optimizing compilers for general-purpose programming languages in
the family of the C programming language.  The initial objective is to
develop this formalization and this certification in the framework of
the calculus of inductive constructions (System Coq) and to take 
advantage of the characteristics of this system to produce certified 
software, for instance with the extraction mechanism.  Applicants should 
have some experience in efficient compilation for high-level languages 
or in the formalization of complex algorithms and some semantic
properties and have some real taste for the other domain.

The post-doct could be done in one of the following team:

- [Lemme, Mimosa, Miró, 
Oasis]@Inria_Sophia_Antipolis
- 
Cristal@Inria_Rocquencourt
- C.P.R.@ CNAM I.I.E (Évry)

The salary is approximately 1800 Euro/month. Candidates can directly contact 
the participants to the action.

More informations on:
http://www-sop.inria.fr/lemme/concert/

********************* Annonce de Post-Doc *********************

L'action de recherche cooperative "Concert" à l'INRIA propose une
bourse doctorale pour les étudiants intéressés dans la formalisation
et la certification de compilateurs optimisant pour des langages de
programmation généralistes de la famille du langage C.  L'objectif
initial est d'effectuer cette formalisation et cette certification
dans le cadre du calcul des constructions inductives (le système Coq),
afin de tirer parti des caractèristiques de ce système pour la
production de logiciel certifié, par exemple à l'aide du mécanisme
d'extraction.  Les candidats intéressés devront apporter des
compétences affirmées dans le domaine de la compilation efficace de
langages de haut-niveau ou dans la preuve sur machine d'algorithmes
complexes et de propriétés sémantiques de programmes et avoir un goût
réel pour l'autre domaine.

Ce stage post-doctoral pourra être effectué dans l'une des équipes
participantes à l'action de recherche, notamment:

- [Lemme, Mimosa, Miró, 
Oasis]@Inria_Sophia_Antipolis
- 
Cristal@Inria_Rocquencourt
- C.P.R.@ CNAM I.I.E (Évry)

La rémunération sera d'environ 1800 Euros/mois. Les candidats peuvent
contacter directement les participants à l'action.

Pour des informations supplémentaires :
http://www-sop.inria.fr/lemme/concert/