[Agda] Two PhD positions in Utrecht

[Wouter Swierstra]

==============================================================
             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 master thesis.

It is possible to apply for this position if you are close to
obtaining your Master's. 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-phd-candidate-position-in-intelligent-tutoring-systems-for-functional-programming-10-fte

The application for the second position is not yet open -- but feel
free to contact me directly if you're interested.

If you're interested in either position, feel free to apply using the
link above; we're happy to discuss which topic fits your interests
best during the application process.