[TYPES/announce] PhD on Lambda-Calculus, in Paris

[Beniamino Accattoli]

Dear colleagues,

There is a 3-years PhD scholarship to work on the lambda-calculus and
its cost models, under my supervision.

The scholarship is funded by the COCA HOLA project
(https://sites.google.com/site/beniaminoaccattoli/coca-hola) whose
other members are

- Ugo Dal Lago (Bologna)
- Delia Kesner (Paris)
- Damiano Mazza (Paris)
- Claudio Sacerdoti Coen (Bologna)

and with whom the candidate will have the opportunity to interact, and
eventually be co-advised.

Roughly, the project is about complexity analyses of beta-reduction,
ranging all the way from abstract (e.g. understanding higher-order
space) and semantical studies (e.g. intersection types for complexity
analyses) to more applied (abstract machines) and even implementative
tasks (hacking the engines of proof assistants with our new
technologies).

Essentially, the topic is a blend of lambda-calculus, functional
programming, linear logic, rewriting, abstract machines, and
complexity analyses. Candidates are expected to have background in at
least one of these areas, and will be let free to pick the research
direction they like the most (among those in the scope of the project,
of course).

The scholarship has to start no later than October 2017.

There is no deadline, just write to me as soon as possible.

The PhD will join the Parsifal INRIA team
(https://team.inria.fr/parsifal/), based in the LIX lab of Ecole
Polytechnique, one of the most prestigious labs in computer science in
France, and located on the outskirts of Paris.