Date : 25/03/02

Auteur de la proposition :Yves Bertot

Unité de recherche ou direction :Sophia Antipolis

Projet ou service d'accueil :Lemme

• Titre de la proposition : PCoq, environnement pour les mathématiques et la déduction
  
  
• Résumé des objectifs et de l'activité (joindre un descriptif détaillé d'au plus 2 pages) :

  L'environnement Pcoq permet le développement de démonstrations mathématiques vérifiées par ordinateur à l'aide du système Coq. Il permet d'aborder des démonstrations mathématiques portant sur des domaines variés: arithmétique, algorithmique, calcul scientifique, propriétés de sécurité de Java et JavaCard, etc.

  Le développement de Pcoq fait suite à celui de CtCoq. CtCoq fournissait un environnement de travail adapté pour d'anciennes versions de Coq et était basé sur Centaur. Le nouvel environnement, développé en Java, a été développé à partir de 1998 et permet maintenant le remplacement de CtCoq, même si la robustesse reste perfectible. Deux ingénieurs ont déjà contribué à ce développement, Pascal Lequang, dans le cadre de la collaboration Génie-II avec Dassault-Aviation et Ahmed Amerkad, ingénieur associé de septembre 2000 à septembre 2002.

  L'accueil d'un ingénieur associé devra permettre une amélioration des conditions de diffusion de logiciel en insistant sur les points suivants:
  • Robustesse de l'outil
  • Facilité d'installation (sur plusieurs plateformes)
  • Etude et corrrection des points faibles d'efficacité (mémoire/temps)
  • Etablissement de procédures systématiques de test
  • Construction de documentation en ligne et tutoriaux

• Environnement (cadre dans lequel s'inscriront les activités, liaison(s) fonctionnelle(s), collaborations internes, relations éventuelles avec des partenaires extérieurs) :

  Le système Pcoq joue un rôle important pour les collaborations de l'équipe Lemme dans deux cadres majeurs:

  1. Le projet européen Mowgli,
  2. L'action de recherche concertée AOC qui débouchera probablement sur d'autres collaborations nationales ou internationales,

• Responsable de l'encadrement : Yves Bertot
  
  
• Compétences et aptitudes requises (formation et spécialité(s), connaissance ou maîtrise d'outils, de techniques, de méthodes et de matériels spécifiques, …..) :

  Programmation objet (Java) et graphique (toolkits)

  
  
  
  
  
• Date visée pour le recrutement : Septembre 2002, Durée projetée (de 6 mois à 12 mois) : 12 mois

• Expliquer en quoi cette expérience est formatrice :
  

  Le travail sur l'environnement Pcoq permet à l'ingénieur de renforcer ses compétences dans la programmation de systèmes interactifs, surtout dans le cadre de la programmation concurrente, rarement utilisée dans les écoles.

  Les expériences menées avec les ingénieurs précédents ont également montré que nous apportions une formation dans les méthodologies de travail: gestion de version, travail en collaboration avec d'autres développeurs (chercheurs sur poste, doctorants), recherche des inefficacités à l'aide d'outils modernes (OptimizeIt, etc).

• Proposer des dispositions de formation et d'accompagnement (cours, conférences, écoles thématiques, tutorat,…) :
  

  L'ingénieur associé pourra recevoir une formation aux méthodes formelles de développements basées sur la démonstration de théorèmes.

  
  
  
• Analyser les perspectives de débouchés professionnels
  

  Nos travaux de développements donnent typiquement une formation complémentaire dans la programmation objet concurrente et les interfaces graphiques. Cette formation est une valeur ajoutée appréciée pour les applications reliées à l'internet. Les perspectives d'emplois pour les ingénieurs formés dans cette direction sont très bonnes (à en juger par les expériences passées).