[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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.yal...@cl.cam.ac.uk) Expected starting date: 1 September 2021