============================================================== Two PhD positions in functional programming ============================================================== The Department of Information and Computing Sciences at Utrecht University is currently advertising two PhD positions in Functional Programming. The candidates will join the Intelligent Systems group, working with Johan Jeuring, Gabriele Keller, and Wouter Swierstra. Besides research, the successful candidate will be expected to help supervise MSc students and assist in the teaching of courses. The positions should be filled by September 2020, although the exact starting date is negotiable. --------------------------------- Research topics --------------------------------- These two positions are tied to two specific topics. * Programming tutors for Functional Languages (Johan Jeuring) The focus of the position is on designing new technologies to support students working in an intelligent tutoring system for functional programming. We expect to use techniques from dependently typed programming, refinement types, program synthesis, automated theorem proving, and more to analyse student programs, and to help students in taking the next step when developing a program. The candidate will investigate the design and use of multiple technologies for this purpose, add them to Ask-Elle, our intelligent tutoring system, perform experiments with the system, and improve the technologies based on the outcome of the experiments. * Compiler verification for a smart contract language (Wouter Swierstra & Gabriele Keller) This project aims to develop a certifying compiler for Plutus Tx, a subset of the purely functional language Haskell that is used to implement smart contracts for the Cardano blockchain. The Plutus smart contract framework is being developed by IOHK for Cardano and the present project is a joint effort of IOHK and Utrecht University. The Plutus Tx compiler is based on the GHC Haskell compiler and adds a translation step from GHC Core to a minimal lambda calculus. Programs in this lambda calculus are executed during transaction validation in a sandboxed execution environment in a manner that is crucial to the security of the blockchain. This project aims to formalise the semantics of the languages involved, to reason about the transformation and optimisation steps that the compiler performs, and finally, to generate a proof object certifying the correctness of the generated code together with that code. --------------------------------- What we are looking for --------------------------------- The ideal candidates should have a degree in Computer Science, be highly motivated, speak and write English well, and be proficient in producing scientific reports. Furthermore, candidates should be able to demonstrate experience with functional programming languages, such as Haskell, OCaml, ML, Agda, Idris, or Coq. --------------------------------- What we offer --------------------------------- The candidates are offered a full-time position for four or five years, depending on the teaching load. The gross salary ranges between €2,325 in the first year and €2,972 in the fourth year per month for full-time employment. A part-time position of at least 0.8 fte may also be possible. The salary is supplemented with a holiday bonus of 8% and an end-of-year bonus of 8.3% per year. The position also includes a generous allocation of fully-paid vacation days. In addition we offer: a pension scheme, partially paid parental leave, and flexible employment conditions. Conditions are based on the Collective Labour Agreement Dutch Universities. The research group will provide the candidate with necessary support on all aspects of the project. More information is available on the website: Terms and employment: http://bit.ly/1elqpM7 Utrecht is consistently ranked as one of the best places in the world to live. --------------------------------- How to apply --------------------------------- To apply please attach a letter of motivation, a curriculum vitae, and (email) addresses of two referees. Make sure to also include a transcript of the courses you have followed (at bachelor and master level), with the grades you obtained, and to include a sample of your scientific writing, such as your MSc or BSc thesis. It is possible to apply for this position if you are close to obtaining your undergraduate degree. In that case include a letter of your supervisor with an estimate of your progress, and do not forget to include at least a sample of your technical writing skills. The application deadline for the first position closes on April 29th. You can apply through the University's website: https://www.uu.nl/en/organisation/working-at-utrecht-university/jobs/5-year-... The application for the second position is not yet open -- but feel free to contact me directly if you're interested. If you're still unsure about the topic, feel free to apply using the link above; we're happy to discuss which topic fits your interests best during the application process.