[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
I am looking for a PhD student to work with me on the CakeML project at the University of Kent in Canterbury, England. The position is part of the "Building Verified Applications in CakeML" project funded by the UK Research Institute in Verified Trustworthy Software Systems: https://vetss.org.uk/funded-proposals/. CakeML (https://cakeml.org) is a formally verified compiler for an ML-like programming language. The studentship is focussed on techniques for formally verifying applications written in the CakeML language. Within the project, there is a wide range of possible topics, ranging from fully automated verification to techniques requiring interactive proof, and also from the logic and mathematics that underpin verification to the creation of a practical verification tool chain. The student will be studying in the University of Kent's programming languages research group which has 13 faculty members, and has notable strengths in verification, concurrency, and functional programming. He or she will also work with the broader international CakeML community at Chalmers (Sweden), CMU (USA), and Data61 (Australia). The position starts in September 2018. Applicants must have, or be about to complete a degree in Computer Science or Mathematics at the BSc or MSc level. The position is fully funded for 3.5 years for students from the UK/EU. Interested candidates should contact me by 21 May, 2018. Scott Owens http://www.cs.kent.ac.uk/~sao