[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
[Posting on behalf of Neel Krishnaswami]
Hello,
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.
Informal enquiries are welcome and should be directed to Dr Neel
Krishnaswami (nk...@cl.cam.ac.uk).
More details and an application form can be found at <
https://www.jobs.cam.ac.uk/job/30485/>.
-------------------------------------------------
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
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.
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 (nk...@cl.cam.ac.uk).
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.
