Cette thèse est financée par l'ANR dans le cadre du projet franco-allemand ANR-DFG FRITES, qui réunit IRIF (CNRS et Université Paris Cité), LMF (Université Paris-Saclay) et RPTU Kaiserslautern-Landau (Allemagne)

Pourquoi ce poste :
Vous développerez la théorie des types ensemblistes (types union, intersection et négation) et du sous-typage sémantique, et la verrez appliquée à des langages réels : ces techniques sont en cours d'intégration dans le compilateur officiel d'Elixir et dans des outils pour Erlang, en collaboration avec les équipes qui développent ces langages (Dashbit et Ericsson). La thèse s'inscrit dans un projet franco-allemand, avec des réunions régulières et des séjours de recherche en Allemagne, et vous permettra de travailler à la fois sur des questions fondamentales et sur leur impact sur des langages utilisés par des dizaines de milliers de développeurs.

Durée et date de début
Le contrat doctoral est d'une durée de 36 mois. La date de début prévue est le 1er décembre 2026.

Rémunération
À partir de 2 300 € brut mensuel, avec possibilité de mission d'enseignement rémunérée (monitorat).

Présentation générale du sujet :

Les langages dynamiques tels que Python, JavaScript, Ruby, Erlang et Elixir sont très utilisés dans l'industrie, y compris pour des systèmes critiques. Leur ajouter des types statiques sans modifier le langage est l'objectif de plusieurs systèmes de types industriels (TypeScript, Flow, Hack, eqWAlizer), qui sont toutefois dépourvus de fondements formels et de garanties de sûreté. L'objectif de FRITES (Flexible and Resilient Integration of Types in Dynamic Language Ecosystems) est de doter les langages dynamiques d'un typage statique fondé sur une base théorique, reposant sur les types ensemblistes et le sous-typage sémantique, où un type est interprété comme l'ensemble des valeurs qui le composent [3,4]. Les unions modélisent les données hétérogènes, les intersections décrivent les fonctions surchargées et les négations servent au raffinement des types après un test. Ces techniques permettent le typage graduel, le polymorphisme paramétrique [5,6] et la reconstruction de types [7].

Elixir [1] et Erlang, qui s'exécutent sur la même machine virtuelle, constituent le principal terrain de validation du projet. Le système de types d'Elixir fondé sur les types ensemblistes [2] est progressivement intégré au compilateur d'Elixir depuis la version 1.17, et le partenaire allemand développe l'outil de typage d'Erlang Etylizer  [12].

La thèse porte sur trois questions complémentaires.

1. Méta-théorie modulaire des types ensemblistes.
La théorie existante ne couvre que des constructeurs élémentaires (fonctions, produits, types de base), alors que les langages réels manipulent des valeurs plus riches : tableaux mutables, dictionnaires, enregistrements [8], objets. Il s'agit de formaliser l'algèbre de types, les opérateurs de types (qui servent à typer les constructeurs et les sélecteurs, tels que l'accès aux champs, le filtrage par motifs et l'application de fonctions), le sous-typage et le « tallying » (résolution de contraintes de sous-typage portant sur des variables de types [6]) de sorte que de nouveaux constructeurs puissent être ajoutés comme des extensions compositionnelles (« plugins »). Chaque extension est munie de ses propres opérateurs et de ses procédures de décision pour le sous-typage et le tallying, et doit s'intégrer au cadre existant sans modifier les composants définis auparavant, tout en préservant la correction, la conservativité et la décidabilité du système. Ce travail sera mené avec le partenaire LMF, qui développera une implémentation de référence efficace de la théorie.

2. Typage des modules.
Il s'agit d'étendre le sous-typage sémantique aux types existentiels du second ordre, outil standard de l'encapsulation des types [9], et de définir un système de types pour les modules de première classe d'Erlang et d'Elixir (modules qui peuvent être passés en argument et renvoyés par des fonctions). L'approche consiste à encoder le système de modules dans un formalisme de type 1ML [11] au moyen des techniques « F-ing modules » [10], puis à réconcilier cet encodage avec l'extension du sous-typage sémantique aux types existentiels. Le système devra prendre en compte le remplacement de code à chaud (hot-code swapping), essentiel pour les applications Erlang et Elixir qui fonctionnent sans interruption et sont mises à jour en cours d'exécution, et s'appliquer de manière cohérente aux deux langages afin de ne pas fragmenter leur écosystème commun. Le typage graduel sera intégré au système de modules en collaboration avec le chercheur ou la chercheuse postdoctorale du projet, qui travaille sur le typage graduel sûr avec effacement des types.

3. Inférence de types.
Le point de départ est l'algorithme de reconstruction de types développé à l'IRIF et au LMF [7], dont le coût est prohibitif sur du code réel en raison de l'espace de recherche exponentiel des arbres d'annotations. Il s'agit de définir des politiques d'application qui réduisent ce coût en restreignant les points où l'inférence polymorphe s'applique (par exemple aux seules frontières des fonctions, ou selon des annotations fournies par le programmeur), et d'étudier le compromis entre puissance de l'inférence et coût.

Les résultats seront présentés dans des article ayant pour vocation à être sousmis pour publication dans les principales conférences et revues du domaine (POPL, ICFP, OOPSLA, TOPLAS, etc.) et pourront être validés par des prototypes intégrés aux outils du projet.

La thèse sera préparée à l'Institut de Recherche en Informatique Fondamentale (IRIF, 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. Elle 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é.

FRITES est un projet de 36 mois mené avec le LMF et avec l'équipe d'Annette Bieniusa à la RPTU Kaiserslautern-Landau. 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 ; une codirection franco-allemande de la thèse pourra être envisagée. 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.

Profil recherché
Master 2 ou diplôme équivalent en informatique fondamentale, obtenu au plus tard à la date de début du contrat. Solides connaissances en théorie des types, en sémantique des langages de programmation et en λ-calcul. Une expérience de la programmation fonctionnelle (OCaml, Haskell, etc.) ou d'un assistant de preuve (Rocq, Agda, Lean, etc.) est appréciée ; la connaissance d'Elixir ou d'Erlang n'est pas requise. Bonne maîtrise de l'anglais scientifique ; la connaissance du français n'est pas exigée.

Les personnes intéressées peuvent candidater sur le site du CNRS Portail Emploi, mais elle sont fortement encouragées à prendre contact avec Giuseppe Castagna et à envoyer un CV et une lettre de motivation. Les documents suivants sont facultatifs mais bienvenus : relevés de notes de master (M1 et M2), mémoire ou rapport de stage de M2, nom et adresse électronique d'une ou deux personnes référentes.

Pour comprendre le type de recherche qui sera développé dans cette thèse, les points de départ sont [2] (principes de conception du système de types d'Elixir) et [3] (une introduction aux types ensemblistes), à lire en premier. Lectures complémentaires suggérées : [6,7] pour l'inférence et [10,11] pour les modules.

• [1]Le langage de programmation Elixir
• [2] Giuseppe Castagna, Guillaume Duboc et José Valim: The Design Principles of the Elixir Type System . The Art, Science, and Engineering of Programming, vol. 8, n. 2, 2024.
• [3] Giuseppe Castagna: Programming with union, intersection, and negation types . Dans The French School of Programming, Springer, 2024, pp. 309–378. ISBN 978-3-031-34517-3.
• [4] Alain Frisch, Giuseppe Castagna et Véronique Benzaken: Semantic Subtyping: dealing set-theoretically with function, union, intersection, and negation types . Journal of the ACM, 55(4):1–64, 2008.
• [5] Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet et Luca Padovani: Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation . POPL '14, pp. 5–17, 2014.
• [6] Giuseppe Castagna, Kim Nguyen, Zhiwu Xu et Pietro Abate: Polymorphic Functions with Set-Theoretic Types. Part 2: Local Type Inference and Type Reconstruction . POPL '15, pp. 289–302, 2015.
• [7] Giuseppe Castagna, Mickaël Laurent et Kim Nguyen: Polymorphic Type Inference for Dynamic Languages . Proc. ACM Program. Lang., 8(POPL), 2024.
• [8] Giuseppe Castagna et Loïc Peyrot: Polymorphic Records for Dynamic Languages . Proc. ACM Program. Lang., 9(OOPSLA1), 2025.
• [9] John C. Mitchell et Gordon D. Plotkin: Abstract types have existential type . ACM Transactions on Programming Languages and Systems, 10(3):470–502, 1988.
• [10] Andreas Rossberg, Claudio Russo et Derek Dreyer: F-ing modules . Journal of Functional Programming, 24(5):529–607, 2014.
• [11] Andreas Rossberg: 1ML - Core and modules united . Journal of Functional Programming, 28, 2018.
• [12] Albert Schimpf, Stefan Wehr et Annette Bieniusa: Set-theoretic Types for Erlang . IFL 2022, ACM, pp. 4:1–4:14, 2023.

Giuseppe Castagna : IRIF, institut de recherche en informatique fondamentale, Université Paris Cité.