Job offer

The thesis will be supervised by Giuseppe Castagna (CNRS senior researcher, IRIF) and co-supervised by Kim Nguyen (associate professor, LMF, Université Paris-Saclay). The student will be enrolled in the doctoral school Sciences Mathématiques de Paris Centre (ED 386) of Université Paris Cité.

The thesis is part of the 36-month ANR-DFG project FRITES, carried out with LMF and with the group of Annette Bieniusa at RPTU Kaiserslautern-Landau, which develops the Etylizer type checker for Erlang. The project includes two plenary meetings per year, alternating between France and Germany, research visits to the German partners, and participation in international conferences. The recruited person will interact with the other PhD students and postdoctoral researchers of the project, as well as with the teams that develop Elixir (Dashbit) and Erlang (Ericsson), with which the partners collaborate.

Set-theoretic types for dynamic languages: meta-theory, modules, and inference

The thesis is part of the French-German ANR-DFG project FRITES (IRIF, LMF, RPTU Kaiserslautern-Landau), whose goal is to equip dynamic languages with static typing built on theoretical foundations, relying on set-theoretic types (union, intersection, negation) and semantic subtyping. These techniques are currently being integrated into the Elixir compiler; Elixir and Erlang are the main validation ground of the project.

The thesis addresses three questions:

1. Modular meta-theory: formalize the type algebra, subtyping, and tallying so that new constructors (arrays, records, objects) can be added as compositional extensions that preserve soundness, conservativity, and decidability.
2. Modules: extend semantic subtyping with second-order existential types and type the first-class modules of Erlang and Elixir (F-ing modules and 1ML techniques), taking hot-code swapping into account.
3. Inference: starting from the type reconstruction algorithm of IRIF and LMF, define policies that reduce the cost of polymorphic inference by restricting where it is applied.

Profile: master’s degree (M2) or equivalent in theoretical computer science, obtained before the start of the contract; solid background in type theory, semantics, and lambda-calculus. Experience with OCaml, Haskell, or a proof assistant is a plus; Elixir and Erlang are not required. Scientific English; French is not required., Research Field Computer science

Education Level Master Degree or equivalent

Research Field Mathematics