[ 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 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.heijlt...@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.heijlt...@bath.ac.uk http://willem.heijltj.es