Doctorant ou doctorante en informatique : types ensemblistes pour les langages dynamiques (H/F)

Description du Poste

Sujet De Thèse

Types ensemblistes pour les langages dynamiques : méta-théorie, modules et inférence

La thèse s'inscrit dans le projet franco-allemand ANR-DFG FRITES (IRIF, LMF, RPTU Kaiserslautern-Landau), qui vise à doter les langages dynamiques d'un typage statique basé sur des fondements théoriques, reposant sur les types ensemblistes (union, intersection, négation) et le sous-typage sémantique. Ces techniques sont en cours d'intégration dans le compilateur d'Elixir ; Elixir et Erlang sont le principal terrain de validation du projet.

La thèse porte sur trois questions :
1. Méta-théorie modulaire : formaliser l'algèbre de types, le sous-typage et le « tallying » de sorte que de nouveaux constructeurs (tableaux, enregistrements, objets) puissent être ajoutés comme des extensions compositionnelles préservant correction, conservativité et décidabilité.
2. Modules : étendre le sous-typage sémantique aux types existentiels du second ordre et typer les modules de première classe d'Erlang et d'Elixir (techniques F-ing modules et 1ML), en tenant compte du remplacement de code à chaud.
3. Inférence : à partir de l'algorithme de reconstruction de types de l'IRIF et du LMF, définir des politiques qui limitent le coût de l'inférence polymorphe en restreignant les points où elle s'applique.

Profil : master 2 ou équivalent en informatique fondamentale, obtenu avant le début du contrat ; solides connaissances en théorie des types, sémantique et lambda-calcul. La pratique d'OCaml, de Haskell ou d'un assistant de preuve est appréciée ; Elixir et Erlang ne sont pas requis. Anglais scientifique ; le français n'est pas exigé.

Votre Environnement de Travail

La personne recrutée sera accueillie à l'Institut de Recherche en Informatique Fondamentale (IRIF, UMR 8243, CNRS et Université Paris Cité), bâtiment Sophie Germain, 8 place Aurélie Nemours, 75013 Paris, au sein du pôle Preuves, programmes et systèmes.

La thèse sera dirigée par Giuseppe Castagna (directeur de recherche CNRS, IRIF) et coencadrée par Kim Nguyen (maître de conférences, LMF, Université Paris-Saclay). Elle sera préparée à l'école doctorale Sciences Mathématiques de Paris Centre (ED 386) de l'Université Paris Cité.

La thèse fait partie du projet ANR-DFG FRITES, d'une durée de 36 mois, mené avec le LMF et avec l'équipe d'Annette Bieniusa à la RPTU Kaiserslautern-Landau, qui développe l'outil Etylizer de typage d'Erlang. Le projet prévoit deux réunions plénières par an, alternativement en France et en Allemagne, des séjours de recherche chez les partenaires allemands et la participation à des conférences internationales. La personne recrutée travaillera en interaction avec les autres doctorants, doctorantes et chercheurs postdoctoraux du projet, ainsi qu'avec les équipes qui développent Elixir (Dashbit) et Erlang (Ericsson), avec lesquelles les partenaires collaborent.

Possibilité de monitorat.

Contraintes et risques

Déplacements ponctuels en France et à l'étranger, en particulier en Allemagne (réunions de projet, séjours de recherche), ainsi que pour des conférences internationales. Aucun risque particulier lié au poste.

Rémunération et avantages

Rémunération

La rémunération est 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

À 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.

Le CNRS

Les métiers de la recherche