This project is proposed in collaboration with Dashbit .

General presentation of the topic:

Type inference for dynamic languages has been a long-standing challenge in programming language research. While ML-style type inference works well for statically-typed functional languages, dynamic languages present unique challenges due to their flexible nature and the presence of dynamic type tests. Recently, a complete type reconstruction system has been developed [1] that combines first-order polymorphism with intersection types, union types, and subtyping based on semantic subtyping [2,3]. This system enables unannotated functions to receive polymorphic types that express overloaded behavior through intersection introduction and support advanced type narrowing via union elimination, making it particularly well-suited for dynamic languages. Since version 1.17, a type system combining first-order polymorphism with intersection types, union types, and subtyping based on semantic subtyping is being integrated into the Elixir programming language [5], a dynamic functional language widely used for building scalable and maintainable applications. However, Elixir's type system currently relies on explicit type annotations with limited use of type inference. Before extending Elixir with the polymorphic type inference system from [1], two critical aspects must be addressed. First, the type reconstruction algorithm has prohibitive computational costs due to the exponential search space of annotation trees, making it impractical for real-world applications. Second, the system in [1] does not support gradual typing, which is essential for languages like Elixir that embrace mixing typed and untyped code.

Objective of the internship:

This internship will focus on addressing the efficiency problem through two complementary approaches: (1) defining application policies that limit inference complexity by restricting where polymorphic inference is applied (e.g., only at function boundaries, or through program\-mer-controlled annotations that guide the reconstruction), and (2) investigating the use of Large Language Models (LLMs) to bootstrap the inference process by generating initial partial annotations from unannotated code, thereby drastically reducing the search space. The first approach requires analyzing the trade-offs between inference power and computational cost. The second transforms the problem from complete reconstruction to refinement and verification of LLM-generated annotations, combining modern AI techniques with rigorous type theory. In practice, this will consist of embedding calls to an LLM oracle within the inference algorithm of [1] via Delphyne, a programming framework for building reliable and modular LLM applications [6,7]. Depending on progress during the internship, the student may also contribute to studying the integration of gradual typing with polymorphic type inference. The creation of a prototype inference engine for Elixir to help programmers migrate their untyped code to typed Elixir would be a valuable bonus.

The research will be jointly supervised at the Karlsruhe Institute of Technology, Karlsruhe, by Jonathan Laurent for the LLM aspects, and at the Research Institute on the Foundations of Computer Science (IRIF) in Paris under the supervision of Giuseppe Castagna for the typing aspects. The modalities for how the intern will share their work and presence between the two institutes will be discussed with the candidate. It will also be pursued in collaboration with José Valim (creator and lead developer of the Elixir programming language, and CEO of Dashbit) as well as Kim Nguyen (LMF, Université Paris Saclay) and Mickaël Laurent (Karl University Prague) who coauthored [1]. The project will explore both theoretical aspects (gradual typing semantics, inference complexity analysis, completeness and soundness proofs) and practical aspects (implementation strategies, LLM integration, application policies), with the balance depending on the candidate's profile. The results of this project are expected to contribute to the broader effort of bringing advanced type systems to dynamic languages, with potential application to the Elixir programming language.

Candidate profile
Advanced knowledge of functional languages and good knowledge of type systems. The student must be able to work in English in order to collaborate with José Valim and the Elixir development team. For the second subject (efficient implementation), some familiarity with LLMs would be beneficial but is not required. Proficiency with dynamic functional programming languages would be an advantage.

The important reference that gives a detailed description of the kind of research that will be developed for this internship is [1] (to be read first) to be complemented with [8]. The mandatory readings are [2] and for the gradual typing extension [4].

• [1] Giuseppe Castagna, Mickaël Laurent, and Kim Nguyen: Polymorphic Type Inference for Dynamic Languages. Proc. ACM Program. Lang., vol. 8, n. POPL, January, 2024.
• [2] Giuseppe Castagna: Programming with union, intersection, and negation types. In The French School of Programming, Springer, August, 2023. ISBN 978-3-031-34517-3.
• [3] 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.
• [4] Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek: Gradual Typing: a New Perspective. Proc. ACM Program. Lang., vol. 3, n. POPL, January, 2019.
• [5] 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.
• [6] Jonathan Laurent, André Platzer: Oracular Programming: A Modular Foundation for Building LLM-Enabled Software. ArXiv, 2025. https://arxiv.org/pdf/2502.05310
• [7] Delphyne: A Python Framework for Oracular Programming. https://github.com/jonathan-laurent/delphyne
• [8] Mickaël Laurent and Jan Vitek: Type inference for functional and imperative dynamic languages. In OOPSLA 2026, to appear.

Giuseppe Castagna : IRIF, Research Institute on the Foundations of Computer Science, Université Paris Cité. Jonathan Laurent (jonathan.laurent@kit.edu, Karlsruhe Institute of Technology).