Research Assistant: £26,715 -£30,942 or Research Associate: £32,816 -£40,322
Fixed-term: The funds for this post are available for 2 years in the first instance with the possibility of extension.
We invite applications for a Postdoctoral Research Associate to join the TypeFoundry project.
The TypeFoundry project aims to use recent developments in proof theory and semantics, such as polarized type theory and call-by-push-value, to identify the theoretical structure underpinning bidirectional type inference.
The overall aim is to develop a theory of type inference capable of scaling up to the support both the wide variety of advanced type system features language designers are interested in (ranging from languages based on sub structural types like Rust to dependent type theories like Agda or Idris), and with a framework for proof which scales beyond kernel calculi all the way up to full-scale languages.
The project will focus on developing and proving the correctness of new bidirectional type inference algorithms; identifying the common categorical/algebraic structure which makes these algorithms work; and using that structure to develop tooling which can automate the generation of type inference algorithms, as well as support mechanised proofs of their correctness.
The position will involve working with TypeFoundry project members (including both PhD students and faculty). It will run initially for 24 months, with the possibility for a further 12 month extension,on any aspect of this project.
The successful candidate is likely to have (or expect to be awarded soon) a PhD in computer science or related discipline, as well as a track record of research expertise in a subset of the following topics:
- Type inference and type theory
- Structural proof theory
- Categorical semantics of programming languages
- Functional programming language implementation
- Use of dependent type theories and proof assistants (eg, Coq or Agda)
Informal enquiries are welcome and should be directed to Dr Neel Krishnaswami (email@example.com).
The University of Cambridge is committed in its pursuit of academic excellence to a proactive and inclusive approach to equality, which supports and encourages all under-represented groups, promotes an inclusive culture, and values diversity.
Expected starting date: 10 October 2021 (or later, to be negotiated with the successful applicant)
Click the 'Apply' button below to register an account with our recruitment system (if you have not already) and apply online.
Please ensure you upload your Curriculum Vitae and a covering letter. If you upload any additional documents which have not been requested, we will not be able to consider these as part of your application.
Please quote reference NR27308 on your application and in any correspondence about this vacancy.
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.Apply online