PhD Position F/M Efficient Space and Garbage Collection for Functional Languages and Lambda Calculi

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.

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.

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.

Knowledge of the lambda calculus, functional programming, and basic concepts of computational complexity and rewriting theory.

- Canteen and cafeteria;

- Sports equipment;

- Transport reimbursement

2100€ gross/month