<div dir="ltr"><div>[Posting on behalf of Neel Krishnaswami]<br></div><div><br></div><div>Hello,</div><br>We have an opening in Cambridge for a postdoctoral position with the ERC Consolidator Grant project TypeFoundry. 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 structures underpinning bidirectional type inference.<br><br>Informal enquiries are welcome and should be directed to Dr Neel Krishnaswami (<a href="mailto:nk480@cl.cam.ac.uk">nk480@cl.cam.ac.uk</a>).<br><br>More details and an application form can be found at <<a href="https://www.jobs.cam.ac.uk/job/30485/">https://www.jobs.cam.ac.uk/job/30485/</a>>.<br><br>-------------------------------------------------<br><br>Research Associate: £32,816 -£40,322<br><br>Fixed-term: The funds for this post are available for 2 years in the first instance with the possibility of extension.<br><br>We invite applications for a Postdoctoral Research Associate to join the TypeFoundry project.<br><br>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.<br><br>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 substructural 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.<br><br>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.<br><br>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.<br><br>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:<br><br>    Type inference and type theory<br>    Structural proof theory<br>    Categorical semantics of programming languages<br>    Functional programming language implementation<br>    Use of dependent type theories and proof assistants (eg, Coq or Agda)<br><br>Informal enquiries are welcome and should be directed to Dr Neel Krishnaswami (<a href="mailto:nk480@cl.cam.ac.uk">nk480@cl.cam.ac.uk</a>).<br><br>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.</div>