[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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.heijlt...@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/
