See the second part of this message for a translation in English. Bourse de doctorat à l'INRIA Sophia Antipolis Projet Lemme le projet Lemme de l'INRIA Sophia Antipolis propose une bourse de doctorat centrée sur les méthodes formelles basées sur Coq et sur la description de langages de programmation adaptés aux cartes à puces. Cette thèse s'intègrera dans le cadre d'une collaboration avec GemPlus, entreprise à la pointe du développement des cartes à puces, Les techniques étudiées devront permettre de développer des vérificateurs de byte-code formellement certifiés pour des langages approximant le langage JavaCard. L'objectif à terme est de fournir un vérificateur de byte-code entièrement prouvé correct pour le langage JavaCard tel qu'il est défini par JavaSun. L'étudiant travaillant avec cette bourse doctorale aura l'occasion d'approfondir ses compétences dans un domaine à l'intersection des domaines théoriques les plus ambitieux de la logique et de l'informatique fondamentale et des champs d'applications les plus dynamiques de l'évolution récente des technologies de l'information et de la communication (authentification, sécurité sur les réseaux, commerce électronique...). Les candidats intéressés devront envoyer un curriculum vitae et une lettre de motivation à Yves Bertot (Yves.Bertot@sophia.inria.fr). Liens utiles: http://www-sop.inria.fr/lemme http://www-sop.inria.fr/lemme/Yves.Bertot http://www.gemplus.com ================== In a collaboration with GemPlus, a leading company in the realm of smartcards, the Lemme Project at INRIA Sophia Antipolis proposes a PhD. grant centered around formal methods based on the Coq proof system and the description of programming languages adapted to smartcards. The studied techniques should make it possible to develop formally certified bytecode verifiers for languages close to JavaCard. The long term objective is to provide a fully formalized bytecode verifier for the whole JavaCard language. The student working on this topic will have the opportunity to strengthen her or his competence in a domain at the frontier between theoretical computer science and the most recent and exciting evolution of information and communication technology. Applications should be sent with a curriculum vitae to Yves Bertot (Yves.Bertot@sophia.inria.fr). For more web links: http://www-sop.inria.fr/lemme http://www-sop.inria.fr/lemme/Yves.Bertot http://www.gemplus.com