Hi, I have a 3-year postdoctoral research position available soon in Cambridge, on type theory and higher categories. The closing date for applications is 13 December, and the position is intended to start early next year, although there is some flexibility in the start date. We have a great group here with lots of category theory--related activity, and Cambridge is a fun place to live. I'd be happy to receive any informal enquiries. Best wishes, Jamie ------------- Research Assistant/Associate in Type Theory for Higher Categories (Fixed Term) https://www.jobs.cam.ac.uk/job/38441/ Fixed-term: The funds for this post are available for 3 years Start Date: 1 January 2023 (or as soon as possible thereafter) Applications are invited for a Research Assistant/Research Associate to work on computational aspects of higher category theory. In this collaborative project, we aim to develop powerful new type-theoretic tools for working with directed globular weak higher categories, such as semistrict languages, cylinder/path space constructions, tensor products, and higher transfors, in particular from the perspective of the Finster-Mimram type theory Catt (arXiv:1706.02866). The position is within Jamie Vicary's research group in the Department of Computer Science at the University of Cambridge. Part of the Cambridge Logical Structures Hub (https://www.cl.cam.ac.uk/research/clash/), this is an exciting scientific environment with many researchers working on related topics, and a vibrant seminar schedule and visitor programme. Cambridge is a beautiful city in which to live and work. The successful candidate is likely to have (or expects to soon be awarded) a PhD in Mathematics, Computer Science or a related discipline. The candidate must have research experience in the following area: - Type-theoretic models of higher category theory Experience in the following areas is desirable: - Cylinder and path space constructions - The Finster-Mimram type theory Catt - Model structures on higher categories - The Gray tensor product of higher categories - Formal proof construction in Agda or Coq - Computads for higher categories - String diagrammatic methods for higher categories For informal enquiries please contact Jamie Vicary (jamie.vicary@cl.cam.ac.uk) Please ensure you upload a covering letter explaining your suitability for the role, a curriculum vitae, and contact information of 2 references. NOTE referees may be contacted at any point of the application process. If you upload any additional documents, which have not been requested, we will not be able to consider these as part of your application. The University actively supports equality, diversity and inclusion and encourages applications from all sections of society. The University has a responsibility to ensure that all employees are eligible to live and work in the UK. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]