PhD student position on proof theory and verification of legal software, Barcelona, Deadline: April 3th, 2022 (AoE) The University of Barcelona offers a 3 year PhD position in collaboration with the Catalan industrial sector. The industrial component of the PhD revolves around the development and verification of legal software in Coq within Formal Vindications SL (formalvindications.com<http://formalvindications.com/>). This work will be complemented with the formalisation of parts of logic/mathematics and possibly research of a less applied nature. As such, there are two possible tracks: (1) The PhD student proposes an external supervisor with whom to work on academic Coq-related questions (such as verified extraction, or others); (2) The PhD student works under the supervision of Joost J. Joosten (joostjjoosten.nl<http://joostjjoosten.nl/>) in the area of proof theory and formal logic for the academic part of the thesis. Gross salary is about 22K€ per year (well above average for a PhD student in Spain) and comes with a travel allowance of at least 2200€ per year. Starting date should be around August/September 2022. The successful candidate will enter an active and strong logic group in Barcelona. They will be trained on Coq and functional programming in OCaml by an experienced team. If needed, the contract can be extended after the initial three years. We are looking for very strong candidates with a background in theoretical computer science, mathematics and/or mathematical logic. It is a strict requirement to have finished a relevant Master degree with an average undergraduate and master score of at least 6.5 out of 10. Interested candidates should send their CV, letter of motivation and academic track record to Aleix Solé <aleix.sole@ub.edu<mailto:aleix.sole@ub.edu>>. Further questions on the position can be sent to Joost J. Joosten <jjoosten@ub.edu<mailto:jjoosten@ub.edu>>. Joost J. Joosten University of Barcelona C. Montalegre 6 08001 Barcelona, Catalonia, Spain Office phone: +34 9340 37984 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]