The Lab for AI and Verification (laiv.uk) at Heriot-Watt University, Edinburgh is looking to fill one PhD post and one postdoctoral post. We are looking for candidates with solid knowledge of Theorem Proving and/or Functional/Logic programming, and enthusiasm to apply this knowledge in the domain of Artificial Intelligence. The PhD post is for 4 years, starting in October 2022. It covers full stipend and PhD fees and is sponsored by the UKRI (ukri.org) and Schlumberger Cambridge (slb.com). The company will provide additional training and support during the PhD studies. This post needs to be filled in as soon as possible. We are also looking to employ a postdoctoral researcher for a 6-12 months project to formalise Criminal law in the Functional Language Catala . Formalising criminal law for autonomous cars is of particular interest. This project will be in collaboration with Jonathan Protzenko, Microsoft Research and the School of Law, Edinburgh University. This project has a flexible starting date. Please direct all queries to Ekaterina Komendantskaya (ek19@hw.ac.uk) Best wishes, Ekaterina