[TYPES/announce] 6-Month postdoc in lambda-calculi and effects, University of Bath

[Willem Heijltjes]

We invite applications for a post-doctoral research position, to investigate a new approach to efficient computation with and without computational effects in the lambda-calculus.

This is a 6-month fixed-term role starting as soon as possible. It is part of the EPSRC-funded project `Typed Lambda-Calculi with Sharing and Unsharing'.

  To apply:   http://www.bath.ac.uk/jobs/Vacancy.aspx?ref=CC8432

  Enquiries:  w.b.heijltjes at bath.ac.uk

  Deadline:   27 July 2021

The project revolves around new ideas in lambda-calculus and functional programming, focused in two areas. The first is *computational effects*, where the project has developed a simple and natural approach that subsumes many existing efforts, called the Functional Machine Calculus (FMC). The second is *efficient computation*, which combines ideas from proof theory and optimal reduction to investigate new, refined type systems for the lambda-calculus.

The background and the source of original ideas is a branch of proof theory called "deep inference", which is closely related to category theory. Knowledge of this area is not essential to the advertised role.

We are looking for excellent candidates with a PhD (or expected to complete one soon) and a proven track record in one or more of the following areas:
 * Lambda-calculus
 * Functional programming theory
 * Computational effects
 * Semantics of programming
 * Deep-inference proof theory

As the successful candidate, you would contribute to one of several potential tasks, for example: 
 * expanding the FMC to a prototype functional language
 * investigating new type systems for the FMC
 * investigating efficient implementations of the FMC
 * further develop type systems towards optimal reduction

You will be part of the Mathematical Foundations group in the Department of Computer Science. We are a small, lively research group with an excellent international reputation. Some of our members are:
  Alessio Guglielmi  http://alessio.guglielmi.name
  Willem Heijltjes   http://willem.heijltj.es
  Jim Laird          http://researchportal.bath.ac.uk/en/persons/james-laird
  Guy McCusker       http://researchportal.bath.ac.uk/en/persons/guy-mccusker
  Thomas Powell      http://t-powell.github.io

Present circumstances permitting, you will have the opportunity to travel to various collaborators on the project in Europe, for example in Bologna and Paris.

The University of Bath is a top-ranking university and a great place to work. Bath is a Unesco World Heritage city with fantastic amenities offering excellent quality of life.

Links:

  Job advert:
     http://www.bath.ac.uk/jobs/Vacancy.aspx?ref=CC8432

  Typed Lambda-Calculi with Sharing and Unsharing:
     http://willem.heijltj.es/Unsharing

  Mathematical Foundations Group:
     http://www.bath.ac.uk/projects/mathematical-foundations-of-computation/

  Department of Computer Science:
     http://www.bath.ac.uk/departments/department-of-computer-science/