Contexte et atouts du poste

Dans le cadre des projets ERC Fresco et AI4Maths soutenu par Renaissance Philanthropy, l'objectif est de développer des techniques de traduction automatique et certifiée entre les assistants à la preuve Lean et Rocq, afin de rendre totalement transparent le fait qu'une bibliothèque mathématique ou logicielle ait été formalisée dans l'un ou l'autre système.

Ce travail s'inscrit dans un contexte de collaboration étroite avec le SIC d'Inria Rennes ainsi qu'avec les équipes Argo, Gallinette et PiCube. Il impliquera des interactions régulières avec ces partenaires et nécessitera des séjours fréquents sur les différents sites afin de favoriser les échanges scientifiques et le développement conjoint des outils et des fondements théoriques associés.

Mission confiée

### Missions

La personne recrutée contribuera au développement de nouvelles méthodes de traduction automatique entre les assistants ...