[TYPES/announce] Post-doctoral position "Typed lambda-calculi with sharing and unsharing" at University of Bath

[Willem Heijltjes]

We invite applications for a post-doctoral research position, to investigate a new approach to sharing in the lambda-calculus based on deep-inference proof theory. This is a 3-year fixed-term post starting 1st of January 2019, part of the EPSRC-funded project `Typed Lambda-Calculi with Sharing and Unsharing'.

  Deadline:   29 October 2018

  Start:      1 January 2019
  Duration:   3 years
  Salary:     Grade 7 - £33,199 rising to £39,609

  Vacancy:    http://www.bath.ac.uk/jobs/Vacancy.aspx?ref=KM6179
  Project:    http://willem.heijltj.es/Unsharing

  Enquiries:  W.B.Heijltjes at bath.ac.uk

  Department of Computer Science
  University of Bath
  United Kingdom


===== Description =====

In recent years, deep inference has made a large impact in proof theory, with spectacular results in proof complexity and normalization for classical logic. In this project we investigate intuitionistic deep inference from a computational perspective, starting from the exciting observation that it can express forms of sharing thus far seen only in sharing graphs for optimal lambda-calculus reduction. We will build on this observation to: develop a theory of normalization with sharing in deep inference, possibly capturing optimality; implement the new means of sharing in typed lambda-calculi, graph-rewriting calculi, and abstract machines; measure their efficiency with semantic tools such as quantitative types.

We are looking for excellent candidates with a PhD and a proven track record in one or more of the following areas:

  * Structural proof theory, particularly deep inference
  * Sharing in the lambda-calculus
  * Sharing graphs and optimal reduction
  * Denotational semantics, particularly quantitative semantics

You will be part of the Mathematical Foundations group in the Department of Computer Science, University of Bath. We are a small, lively research group with an excellent international reputation. You will have the opportunity to travel to various collaborators on the project in Europe, for example in Bologna, Oslo, and Paris.

The University of Bath is a great place to work with outstanding facilities. Bath is a Unesco World Heritage city with fantastic amenities offering excellent quality of life.


===== Relevant links =====

  Project page   
    http://willem.heijltj.es/Unsharing

  Mathematical Foundations group
    http://www.bath.ac.uk/comp-sci/research/mathematical-foundations/

  Deep Inference
    http://alessio.guglielmi.name/res/cos/


===== Applications =====

To apply, use the online form on the vacancy page.

  Vacancy
    http://www.bath.ac.uk/jobs/Vacancy.aspx?ref=KM6179

  Job Description & Person Specification
    (MS WORD) http://www.bath.ac.uk/jobs/Upload/vacancies/files/13812/Job%20description%20RA.docx
    (PDF)     http://willem.heijltj.es/Unsharing/pdf/Job_description_Unsharing.pdf

Applications close 29 October. Interview dates are to be determined. Please also consider the following.

  Terms of Employment
    http://www.bath.ac.uk/jobs/display.aspx?id=1201&pid=0


===== Enquiries =====

For any questions about the position, the project, or the recruitment process, please contact:

  Willem Heijltjes
  Department of Computer Science
  University of Bath

  W.B.Heijltjes at bath.ac.uk
  http://willem.heijltj.es