[TYPES/announce] Postdoc position at Cambridge in programming with equations

[Jeremy Yallop]

We have an opening in Cambridge for a researcher on the Frex project
(https://www.cl.cam.ac.uk/~jdy22/projects/frex).  Informal enquiries
are welcome: please feel free to get in touch.

---------------------------------------------------------------------------------------------------
Research Assistant / Associate in Programming with Equations (Fixed Term)
https://www.jobs.cam.ac.uk/job/29773/

Applications are invited for a Research Assistant/Associate to join
the Frex project.

The Frex project investigates the use of equations in programming.
There is often a large gap between what programmers know about their
programs and what compilers are able to deduce.  Frex targets this gap
by exposing to the compiler the equations proved by programmers about
programs so that they can be used to improve optimisation and type
checking.

The position will involve working with Frex project members at the
Universities of Cambridge, Edinburgh and St Andrews to extend and
improve the design and implementations of Frex. Work up to this point
has focused on equations for first-order single-sorted algebras and we
plan to extend the techniques to more elaborate settings.

The successful candidate is likely to have (or expect to be awarded
soon) a PhD in computer science or a related discipline, as well as a
track record of published research and experience or demonstrable
interest in some combination of the following:

- Dependently typed programming languages or proof assistants based on
type theory (e.g. Agda, Idris, Coq, Lean)

- Functional programming languages (e.g. F#, OCaml, Haskell)

- Partial evaluation, normalization by evaluation, multi-stage
programming, supercompilation or related techniques

- Algebraic structures, universal algebra and categorical algebra

Informal enquiries are welcome and should be directed to Dr Jeremy
Yallop (jeremy.yallop at cl.cam.ac.uk)

Expected starting date: 1 September 2021