Informations générales
Intitulé de l'offre : Ingénieur (H/F) - développement d’extensions de la théorie équationnelle de l’assistant à la preuve Rocq
Référence : UMR7351-ISADEA-001
Nombre de Postes : 1
Lieu de travail : PARIS
Date de publication : jeudi 19 décembre 2024
Type de contrat : IT en contrat CDD
Durée du contrat : 12 mois
Date d'embauche prévue : 1 février 2025
Quotité de travail : Complet
Rémunération : Entre 2 875 € et 3550 € bruts mensuels selon expérience
Niveau d'études souhaité : BAC+5
Expérience souhaitée : Indifférent
BAP : E - Informatique, Statistiques et Calcul scientifique
Emploi type : Chef-fe de projet ou expert-e en Ingéniérie logicielle
Missions
Le projet a pour objet de participer au développement d’extensions de la théorie équationnelle de l’assistant à la preuve Rocq, en lien avec la théorie des types cubiques et des outils de la réécriture. Le candidat mettra en œuvre ses connaissances et compétences en théorie des types, formalisation des mathématiques et programmation fonctionnelle.
Activités
- Mise en place d’outils de réécriture modulo dédiés au sein de l’écosystème Rocq
- Intégration de ces outils de réécriture à la théorie des types dépendants
- Formalisation en Rocq de modules de théorie des types cubiques
- Comparaison entre formalisation cubique et simplicial de l’axiome d’univalente
- Etude bibliographique et comparaisons entre différentes approches logicielles
- Organisation d’ateliers / de conférences.
- Publication d’un compte-rendu final.
Compétences
• Techniques et sciences de l'ingénieur en informatique,
• Formalisation des mathématiques (connaissance souhaitable)
• Théorie des types dépendants (connaissance approfondie)
• Assistants à la preuve (connaissance générale)
• Anglais : B2 (Cadre européen de référence)
• Capacité de conceptualisation
• Sens critique
• Sens de l'organisation
• Aptitude au travail en équipe
Contexte de travail
laboratoire de recherche
Contraintes et risques
N/A