PhD student in computer science: set-theoretic types for dynamic languages (M/F)

Job Description

Thesis Subject

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.

Your Work Environment

The recruited person will work at the Institut de Recherche en Informatique Fondamentale (IRIF, UMR 8243, CNRS and Université Paris Cité), Bâtiment Sophie Germain, 8 place Aurélie Nemours, 75013 Paris, in the "Proofs, programs and systems" research pole.

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.

Constraints and risks

Occasional travel in France and abroad, in particular to Germany (project meetings, research visits), and to international conferences. No specific risk associated with the position.

Compensation and benefits

Compensation

2300 € gross monthly

Annual leave and RTT

44 jours

Remote Working practice and compensation

Pratique et indemnisation du TT

Transport

Prise en charge à 75% du coût et forfait mobilité durable jusqu’à 300€

About the offer

About the CNRS

The CNRS is a major player in fundamental research on a global scale. The CNRS is the only French organization active in all scientific fields. Its unique position as a multi-specialist allows it to bring together different disciplines to address the most important challenges of the contemporary world, in connection with the actors of change.

CNRS

The research professions