PhD student position on verification of legal software, Barcelona (Spain)

The University of Barcelona offers a 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. This work will be complemented with the formalization of parts of logic/mathematics. We are looking for candidates with a background in theoretical computer science and/or mathematical logic. Apart from the required knowledge of Coq and Ocaml, other IT skills are recommended, especially knowledge/experience with other functional programming languages.

We offer a three-year position in the PhD program in Mathematics and Computer Science which is located in the very center of Barcelona. The group where this project will be embedded works on ordinal analysis via modal logic and reflection principles; we expect collaboration with the main group to arise, but we are open to alternative proposals. The PhD student will be part of a large and active research group led by Joost J. Joosten.  If after three years the PhD has not been finished, but there is realistic expectations that it will be finished soon, the company will consider continuing the position in its major characteristics. Apart from the usual PhD trajectory, the candidates will participate in cutting edge formalization developments in an industrial setting.