Doctorat en mathématiques et informatique fondamentale (H/F)
Nouveau
- CDD Doctorant
- 36 mois
- Doctorat
This offer is available in English version
Cette offre est ouverte aux personnes disposant d’un titre leur reconnaissant la qualité de travailleur handicapé ou travailleuse handicapée.
L'offre en un coup d'oeil
L'unité
Institut de Recherche en Informatique Fondamentale
Type de Contrat
CDD Doctorant
Temps de Travail
Complet
Lieu de Travail
75205 PARIS 13
Durée du contrat
36 mois
Date d'Embauche
01/11/2026
Rémuneration
La rémunération est d'un minimum de 2300,00 € mensuel
Postuler Date limite de candidature : mercredi 14 octobre 2026 23:59
Description du Poste
Sujet De Thèse
Dualité linéaire et effets algébriques supérieurs en théorie des types homotopiques
L’objectif de cette thèse sera de définir un cadre unifié, syntaxique et fonctoriel, qui intègre logique linéaire, effets algébriques, et théorie des types homotopiques. On partira pour cela de l’interprétation sémantique d’un système de types dépendants avec univers Type : Type donné dans le langage de la théorie des domaines. Il s’agira tout d’abord d’axiomatiser les structures et propriétés de cette interprétation, et de dégager le lien avec le modèle relationnel de la logique linéaire. On formulera ensuite des extensions de la théorie des types dépendants avec types intersection, en s’appuyant sur la correspondance entre types intersections et éléments finis de la sémantique relationnelle. En parallèle, on étudiera les liens entre continuations linéaires, dualité dans les jeux de dialogue et effets algébriques supérieurs, dans le cadre d'une théorie des types homotopique et multimodale.
Compétences:
• Bonne connaissance de la théorie et de la sémantique des types dépendants avec égalité
• Bonne connaissance d’un assistant de preuve tel que Agda, Isabelle, Lean ou Rocq sur les aspects formalisation et implémentation interne
• Bonne connaissance d’un ou plusieurs langages de programmation et de spécification tels que Haskell, OCaml, Rust
• Anglais : B2 (Cadre européen de référence)
• Capacité de conceptualisation
• Sens critique
• Sens de l'organisation
• Aptitude au travail en équipe
Votre Environnement de Travail
Le projet a pour objectif de participer au développement d’une nouvelle génération d’assistants à la preuve, qui intègrent dans leurs noyaux une couche linguistique et des outils d'assistance automatisée pour guider le scientifique et faciliter la construction de documents mathématiques certifiés, depuis le choix des concepts et des définitions, jusqu’à l'élaboration des théorèmes et des démonstrations.
Contraintes et risques
Aucuns
Rémunération et avantages
Rémunération
La rémunération est d'un minimum de 2300,00 € mensuel
Congés et RTT annuels
44 jours
Pratique et Indemnisation du TT
Pratique et indemnisation du TT
Transport
Prise en charge à 75% du coût et forfait mobilité durable jusqu’à 300€
À propos de l’offre
| Référence de l’offre | UMR8243-LAUPIN-004 |
|---|---|
| Section(s) CN / Domaine de recherche | Sciences informatiques : fondements de l'informatique, calculs, algorithmes, représentations, exploitations |
À propos du CNRS
Le CNRS est un acteur majeur de la recherche fondamentale à une échelle mondiale. Le CNRS est le seul organisme français actif dans tous les domaines scientifiques. Sa position unique de multi-spécialiste lui permet d’associer les différentes disciplines pour affronter les défis les plus importants du monde contemporain, en lien avec les acteurs du changement.
Créer une alerte
Ne manquez aucune opportunité de trouver le poste qui vous correspond. Inscrivez-vous gratuitement et recevez les nouvelles offres directement dans votre boite mail.