Ce poste est proposé en collaboration avec Dashbit , Remote et ValoCité Lab&Co.

Why this position:
You will work directly with José Valim, the creator of Elixir, and the Elixir core team, to design and implement the type system for one of today's fastest-growing production programming languages. This is a rare opportunity to combine deep programming-language theory — semantic subtyping, gradual typing — with real-world impact: the system you build will ship in the official Elixir compiler and reach tens of thousands of developers worldwide.

Duration and starting date
The position is for 12 months, with the possibility of an extension of a few months. The expected starting date is 1 November 2026; this date can be negotiated but only postponed, not brought forward.

Remuneration
Based on experience, according to the CNRS salary scale – approx. 2 890 € net/month (less than 2 years of post-doctoral experience) to 3 520 € net/month (2 to 7 years of post-doctoral experience)

General presentation of the topic:

Elixir is an open-source dynamic functional programming language that runs on the Erlang Virtual Machine [1], designed for building scalable and maintainable applications. Its characteristics have earned it a surging adoption by hundreds of industrial actors and tens of thousands of developers, including companies such as Apple, Discord, PepsiCo, BBC, Adobe, and Spotify. Static typing is nowadays the most requested feature from the Elixir community. IRIF has an ongoing collaboration with the Elixir development team to define and implement static type-checking for Elixir, described in [2]. It is a type system based on the theory of semantic subtyping [4,5], thanks to which union, intersection, and negation types (a.k.a. set-theoretic types) can be added to existing languages. It features cutting edge typing techniques: parametric polymorphism with local type inference, overloading, occurrence typing, gradual typing, and a sophisticated type analysis of patterns and guards. This system has been progressively integrated into Elixir since the June 2024 release of version 1.17, and continues to evolve with each new release. Elixir features a powerful module system with first class modules, whose typing is under development. This is the subject of this project.

Elixir's module system is currently being extended with a type system based on the approach described in Andreas Rossberg's "1ML - Core and modules united" [6]. This work follows from two previous internships aiming at establishing the foundation for typing Elixir's modules using 1ML's unified approach, where modules and values are treated uniformly within a single type-theoretic framework. As part of the TME (Typing Modules for Elixir) project, funded by ValoCité Lab&Co, the postdoctoral researcher will be hired at IRIF to extend Elixir's semantic set-theoretic type system to the language's module system. This implies completing the existing work on the module type system and targeting two major scientific challenges:

• Gradual typing integration: extending the module type system to support the seamless mixing of typed and untyped code central to Elixir's gradual typing philosophy.
• Semantic subtyping foundations: integrating existential types — used in the module system to encode abstract data types and information hiding — into the semantic subtyping framework underlying Elixir's core type system.

We thus propose two parallel but tightly related subjects of investigation.

Gradual typing integration for Elixir's module system.
The first subject aims to extend the module type system to support gradual typing, adapting the techniques from [2,3] to the module context, thereby enabling seamless integration of typed and untyped modules consistent with Elixir's gradual typing philosophy. This will allow developers to gradually add types to their modules while maintaining compatibility with untyped code, following Elixir's philosophy of progressive type adoption.

Semantic subtyping foundations for existential types.
The second subject (much more difficult) is to study how to integrate existential types—which encode abstract data types and information hiding in the module system—into the semantic subtyping framework [4,5]. This would require proving that the subtyping relation induced by the module system (based on 1ML) coincides with the subtyping relation derived from the semantic interpretation of existential types, thus reconciling these two approaches and ensuring that the module type system aligns with Elixir's core type system at a foundational level.

The research will be carried out at the Research Institute on the Foundations of Computer Science (IRIF) in Paris under the supervision of Giuseppe Castagna (principal investigator for the Elixir Type System, directeur de recherche CNRS at IRIF) and in collaboration with José Valim (creator and main developer of the Elixir programming language, CEO of Dashbit and Remote's Technical Advisor) and Guillaume Duboc (who develops the Elixir type system). The project will explore both theoretical (theory of gradual typing, extension of semantic subtyping) and practical (e.g., language and module typing system design and implementation) aspects, in a proportion that will depend on the profile of the candidate. The perspective of this proposal is that the results of this project will be integrated in the compiler of Elixir.

Candidate profile
A PhD in Computer Science or a related field is required by the start of the position (not necessarily at the time of application). Advanced knowledge of functional languages and basic knowledge of type systems. The candidate must be proficient in English in order to collaborate with José Valim and the development team of Elixir. Proficiency with Elixir or Erlang programming languages is not necessary but would be a clear advantage.

You can directly apply at the CNRS site of Portail Emploi , but candidates are strongly recommended to contact Giuseppe Castagna before applying. The formal application on the CNRS site should include a CV (with a list of publications) and a motivation letter.

The important references that give a detailed description of the kind of research that will be developed for this postdoc position are [2] (design principles) and [3] (technical foundations), to be read first. Further suggested readings are [4,6,7].

• [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, March 2024. To appear.
• [3] Giuseppe Castagna and Guillaume Duboc: Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir . Submitted, March 2025.
• [4] Giuseppe Castagna: Programming with union, intersection, and negation types. In The French School of Programming, Springer, August, 2023. ISBN 978-3-031-34517-3.
• [5] G. Castagna: Covariance and Contravariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers) . Logical Methods in Computer Science, n. 16, pag. 15:1–15:58, 2020.
• [6] Andreas Rossberg: 1ML - Core and modules united. Journal of Functional Programming, 28, 2018.
• [7] Clément Blaudeau, Didier Rémy, and Gabriel Radanne. Fulfilling OCaml modules with Transparency. Proc. ACM Program. Lang., 8(OOPSLA1):194--222, 2024.

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