Postdoctoral Researcher in Type Theory for Dynamic Languages M/F

Job Description

Missions

Elixir is an open-source dynamic functional programming language 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. Static typing is nowadays the top priority request from the Elixir community and IRIF has an ongoing collaboration with the Elixir development team to define and implement static type-checking for Elixir.

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. Two major scientific challenges are targeted:
(1) integrating gradual typing into the module system, enabling seamless mixing of typed and untyped modules;
(2) integrating existential types — needed to encode abstract data types and information hiding — into the semantic subtyping framework.

The postdoc will work under the supervision of Giuseppe Castagna (CNRS Research Director, IRIF), in close collaboration with Guillaume Duboc (developer of Elixir's current type system) and José Valim (creator of Elixir).

More information at https://www.irif.fr/~gc/postdocElixirModules.en.html

Activity

- Develop the theoretical foundations of the type system for Elixir's modules, in particular: (1) integrating gradual typing into the module system, adapting existing techniques to enable seamless coexistence of typed and untyped modules; (2) integrating existential types — used to encode abstract data types and information hiding — into the semantic subtyping framework.
- Implement a proof-of-concept prototype of the typed module system and progressively integrate it into official Elixir releases, in collaboration with Guillaume Duboc and José Valim.
- Conduct case studies on major Elixir projects (including Remote's codebase, 1M+ lines of code) to validate performance and bug detection rates; write scientific publications for top-tier international conferences

Your Profil

Skills

- Strong background in type theory and programming language semantics.
- Experience in functional programming language research; interest in dynamic languages and module systems. Knowledge of Elixir or Erlang is an asset but not required.
- Very good command of scientific English (reading, writing, speaking), required for collaboration with José Valim and the Elixir development team; ability to work in an international academic-industry research environment.

Your Work Environment

The postdoctoral researcher will be based at IRIF (Sophie Germain Building, Université Paris Cité, Paris 13th arrondissement). He or she will work as part of a team with Guillaume Duboc and will engage in regular discussions with José Valim (creator of Elixir, one day per week via videoconference). Access to IRIF's computing resources. Occasional travel for conferences (funded by the project).

Contact : Giuseppe Castagna

Compensation and benefits

Compensation

According to CNRS salary scale (2 to 7 years post-doctoral experience) – From 3131€ grossly per month

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