This PhD is funded by the ANR within the French-German ANR-DFG project FRITES, which brings together IRIF (CNRS and Université Paris Cité), LMF (Université Paris-Saclay), and RPTU Kaiserslautern-Landau (Germany)

Why this position:
You will develop the theory of set-theoretic types (union, intersection, and negation types) and semantic subtyping, and see it applied to real languages: these techniques are being integrated into the official Elixir compiler and into tools for Erlang, in collaboration with the teams that develop these languages (Dashbit and Ericsson). The thesis is part of a French-German project, with regular meetings and research visits in Germany, and gives you the opportunity to work at the same time on foundational questions and on their impact on languages used by tens of thousands of developers.

Duration and starting date
The doctoral contract is for 36 months. The expected starting date is 1 December 2026.

Remuneration
From 2 300 € gross/month, with the possibility of additional paid teaching (monitorat).

General presentation of the topic:

Dynamic languages such as Python, JavaScript, Ruby, Erlang, and Elixir are widely used in industry, including for mission-critical systems. Adding static types to them without changing the language is the goal of several industrial type systems (TypeScript, Flow, Hack, eqWAlizer), which however lack formal foundations and safety guarantees. The goal of FRITES (Flexible and Resilient Integration of Types in Dynamic Language Ecosystems) is to equip dynamic languages with static typing built on theoretical foundations, relying on set-theoretic types and semantic subtyping, where a type is interpreted as the set of its values [3,4]. Unions model heterogeneous data, intersections describe overloaded functions, and negations are used for type narrowing. These techniques support gradual typing, parametric polymorphism [5,6], and type reconstruction [7].

Elixir [1] and Erlang, which run on the same virtual machine, are the main validation ground of the project. The type system of Elixir based on set-theoretic types [2] has been progressively integrated into the Elixir compiler since version 1.17, and the German partner develops the Etylizer type checker for Erlang [12].

The thesis addresses three complementary questions.

1. Modular meta-theory of set-theoretic types.
The existing theory covers only elementary constructors (functions, products, basic types), while real languages manipulate richer values: mutable arrays, dictionaries, records [8], objects. The goal is to formalize the type algebra, the type operators (used to type constructors and selectors such as field access, pattern matching, and function application), subtyping, and tallying (solving subtyping constraints on type variables [6]) so that new constructors can be added as compositional extensions ("plugins"). Each extension comes with its own operators and decision procedures for subtyping and tallying, and must integrate into the framework without modifying the previously defined components, while preserving soundness, conservativity, and decidability. This work will be carried out with the LMF partner, who will develop an efficient reference implementation of the theory.

2. Typing modules.
The goal is to extend semantic subtyping with second-order existential types, the standard tool for type encapsulation [9], and to define a type system for the first-class modules of Erlang and Elixir (modules that can be passed as arguments and returned by functions). The approach is to encode the module system in a 1ML-like formalism [11] by using F-ing techniques [10], and then to reconcile this encoding with the extension of semantic subtyping with existential types. The system must take into account hot-code swapping, which is essential for long-running Erlang and Elixir applications that are upgraded while they run, and must apply consistently to both languages so as not to fragment their common ecosystem. Gradual typing will be integrated into the module system in collaboration with the postdoctoral researcher of the project, who works on sound gradual typing with type erasure.

3. Type inference.
The starting point is the type reconstruction algorithm developed at IRIF and LMF [7], whose computational cost is prohibitive for real code because of the exponential search space of annotation trees. The goal is to define application policies that reduce this cost by restricting where polymorphic inference is applied (for instance, only at function boundaries, or according to annotations provided by the programmer), and to study the trade-off between inference power and cost.

The results will be presented in articles with the goal of submitting them for publication in the main conferences and journals of the field (POPL, ICFP, OOPSLA, TOPLAS, etc.) and may be validated by prototypes integrated into the tools of the project.

The thesis will be prepared at the Research Institute on the Foundations of Computer Science (IRIF, CNRS and Université Paris Cité), Bâtiment Sophie Germain, 8 place Aurélie Nemours, 75013 Paris, in the "Proofs, programs and systems" research pole. It will be supervised by Giuseppe Castagna (directeur de recherche CNRS, IRIF) and co-supervised by Kim Nguyen (maître de conférences, 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é.

FRITES is a 36-month project carried out with LMF and with the group of Annette Bieniusa at RPTU Kaiserslautern-Landau. The project includes two plenary meetings per year, alternating between France and Germany, research visits to the German partners, and participation in international conferences; a joint French-German supervision of the thesis may be considered. The student 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.

Candidate profile
Master's degree (M2) or equivalent in theoretical computer science, obtained no later than the start date of the contract. Solid background in type theory, programming language semantics, and λ-calculus. Experience with functional programming (OCaml, Haskell, etc.) or with a proof assistant (Rocq, Agda, Lean, etc.) is a plus; knowledge of Elixir or Erlang is not required. Good command of scientific English; knowledge of French is not required.

You can directly apply at the CNRS site of Portail Emploi, but interested candidates are strongly advised to contact Giuseppe Castagna and send a CV and a motivation letter. The following documents are optional but welcome: master's transcripts (M1 and M2), master's thesis or internship report, and the name and email address of one or two referees.

Good starting points to understand the kind of research that will be developed in this thesis are [2] (design principles of the Elixir type system) and [3] (an introduction to set-theoretic types), to be read first. Further suggested readings are [6,7] for inference and [10,11] for modules.

• [1]The Elixir Programming Language
• [2] Giuseppe Castagna, Guillaume Duboc, and 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 . In The French School of Programming, Springer, 2024, pp. 309–378. ISBN 978-3-031-34517-3.
• [4] Alain Frisch, Giuseppe Castagna, and 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, and 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, and 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, and Kim Nguyen: Polymorphic Type Inference for Dynamic Languages . Proc. ACM Program. Lang., 8(POPL), 2024.
• [8] Giuseppe Castagna and Loïc Peyrot: Polymorphic Records for Dynamic Languages . Proc. ACM Program. Lang., 9(OOPSLA1), 2025.
• [9] John C. Mitchell and 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, and 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, and Annette Bieniusa: Set-theoretic Types for Erlang . IFL 2022, ACM, pp. 4:1–4:14, 2023.

Giuseppe Castagna : IRIF, Research Institute on the Foundations of Computer Science, Université Paris Cité.