PhD Position F/M Efficient Space and Garbage Collection for Functional Languages and Lambda Calculi
Type de contrat : CDD
Niveau de diplôme exigé : Bac + 5 ou équivalent
Fonction : Doctorant
A propos du centre ou de la direction fonctionnelle
The Inria Saclay-Île-de-France Research Centre was established in 2008. It has developed as part of the Saclay site in partnership with Paris-Saclay University and with the Institut Polytechnique de Paris.
The centre has 40 project teams , 32 of which operate jointly with Paris-Saclay University and the Institut Polytechnique de Paris; Its activities occupy over 600 people, scientists and research and innovation support staff, including 44 different nationalities.
Mission confiée
Functional programming languages are expressive languages rooted in mathematical concepts and fostering a high-level approach to programming, for which some of the low-level aspects of programming are taken care of automatically by the language.
One of the features is that the programmer does not need to manually dispose of the allocated memory, as happens for instance in imperative languages such as C, since there is an underlying garbage collector taking care of it. While this is a relief for the programmer and prevents many runtime errors, it then becomes harder to predict the space usage of functional programs, and it also forces the implementers of the language to design an efficient garbage collector.
The framework underlying functional languages is the lambda calculus, a mathematical setting that does not come with a low-level machine model. Until very recently, it was unclear how to reasonably measure the time and space complexity of programs expressed as terms of the lambda calculus (where reasonably means in a way equivalent to that of Turing machines), because of its high-level nature, and, consequently, also for functional programs.
After considerable recent progress on the understanding of time complexity for the lambda calculus, in 2022 Accattoli, Dal Lago, and Vanoni obtained the first reasonable space cost model for it, via the introduction of an unusual abstract machine, dubbed Space KAM (standing for Krivine abstract machine). Their work develops a very fine analysis of the space consumption of the lambda calculus, taking into account garbage collection.
In a second work, Accattoli, Dal Lago, and Vanoni also showed how to abstract away from the details of the Space KAM and capture its space consumption on a lambda term T via a type system for the lambda calculus.
Principales activités
The notion of space at work in Accattoli, Dal Lago, and Vanoni’s theoretical result is reasonable, and yet it is not necessarily efficient for ordinary functional programs. The key point is that, for being reasonable, one needs a space cost model and a notion of execution that efficiently simulates Turing machines, but ordinary lambda terms and functional programs tend to work in a way that is inherently different from the special lambda terms that simulate Turing machines. In particular, the execution of general lambda terms crucially rely on sharing of sub-terms, which is instead useless, and actually induces inefficiencies, when one wants to only simulate Turing machines.
The aim of the PhD is to partly depart from the work on reasonable space for the lambda calculus and develop a theoretical study of the efficient space consumption of lambda terms and functional programs. The idea is to consider as acceptable notions of space that might be slightly unreasonable, that is, not necessarily efficient in the specific case of the encoding of Turing machines, but more efficient in general, by exploiting forms of sub-term sharing.
Various ingredients play a role. One is garbage collection. It turns out that, while garbage collection is studied in the compilation of programs, it is usually ignored in the study of abstract machines (which rather model the interpretation of programs), since abstract machines have mainly been studied in relation to time. Therefore, a first topic to explore would be developing abstract machines with garbage collection (and sharing).
Another one is the time / space trade-off. Typically, a minimal use of space requires repeating tasks to retrieve information that has not been stored (because of minimality), thus degrading the time performance. Vice-versa, annotating information in the data structures used to execute programs (which degrade the space performance) allows one to lower the time cost. It is then interesting to study the trade-off between time and space, classifying different execution schemas with respect to their asymptotic overhead.
A related theoretical topic is the modeling via type systems of the space consumptions of these space-efficient machines, by building on the second result by Accattoli, Dal Lago, and Vanoni.
A more practical direction is to try to build a bridge with the real functional programming languages and how they handle space-efficiency and garbage collection. For this, Gabriel Scherer (chargé de recherche in the Picube Inria team, previously a member of the Partout team), who is one of the main contributors to the maintenance of the OCaml functional programming language, shall be the co-adivsor of the PhD, balancing the theoretical perspective provided by Accattoli, the main advisor.
Compétences
Knowledge of the lambda calculus, functional programming, and basic concepts of computational complexity and rewriting theory.
Avantages
- Canteen and cafeteria;
- Sports equipment;
- Transport reimbursement
Rémunération
2100€ gross/month
Informations générales
- Thème/Domaine : Preuves et vérification
- Ville : Palaiseau
- Centre Inria : Centre Inria de Saclay
- Date de prise de fonction souhaitée : 2024-10-01
- Durée de contrat : 3 ans
- Date limite pour postuler : 2024-09-30
Attention: Les candidatures doivent être déposées en ligne sur le site Inria. Le traitement des candidatures adressées par d'autres canaux n'est pas garanti.
Consignes pour postuler
Sécurité défense :
Ce poste est susceptible d’être affecté dans une zone à régime restrictif (ZRR), telle que définie dans le décret n°2011-1425 relatif à la protection du potentiel scientifique et technique de la nation (PPST). L’autorisation d’accès à une zone est délivrée par le chef d’établissement, après avis ministériel favorable, tel que défini dans l’arrêté du 03 juillet 2012, relatif à la PPST. Un avis ministériel défavorable pour un poste affecté dans une ZRR aurait pour conséquence l’annulation du recrutement.
Politique de recrutement :
Dans le cadre de sa politique diversité, tous les postes Inria sont accessibles aux personnes en situation de handicap.
Contacts
- Équipe Inria : PARTOUT
-
Directeur de thèse :
Accattoli Beniamino / Beniamino.Accattoli@inria.fr
A propos d'Inria
Inria est l’institut national de recherche dédié aux sciences et technologies du numérique. Il emploie 2600 personnes. Ses 215 équipes-projets agiles, en général communes avec des partenaires académiques, impliquent plus de 3900 scientifiques pour relever les défis du numérique, souvent à l’interface d’autres disciplines. L’institut fait appel à de nombreux talents dans plus d’une quarantaine de métiers différents. 900 personnels d’appui à la recherche et à l’innovation contribuent à faire émerger et grandir des projets scientifiques ou entrepreneuriaux qui impactent le monde. Inria travaille avec de nombreuses entreprises et a accompagné la création de plus de 200 start-up. L'institut s'efforce ainsi de répondre aux enjeux de la transformation numérique de la science, de la société et de l'économie.