Two Industrial PhD Student Positions in Formal Logic at the University of Barcelona

The University of Barcelona offers two PhD positions in collaboration with the Catalan industrial sector. As such, the industrial component of the PhD revolves around the development and verification of legal software in Coq. This work will be complemented with the formalization of parts of logic/mathematics. Since 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.

We offer two three-year positions in the PhD program in Mathematics and Computer Science which is located in the very center of Barcelona. Apart from the usual PhD trajectory, the candidates will participate in cutting-edge developments in formalization in an industrial setting. The travel allowances can vary to over 2200 € per year and the gross salary varies between 18 K and 22 K per year, depending on how much financial support this project will receive from the Catalan authorities. Incorporation should take place between November 2016 and February 2017.

We are looking for candidates with a background in theoretical computer science and/or mathematical logic. It is a strict requirement to have finished a relevant Master with an average score of at least 6.5 (out of 10) over all courses taken in both the master and undergraduate studies. Apart from the required knowledge of Coq and Ocaml, other IT skills are recommended, especially knowledge/experience with other functional programming languages. Previous commercial work experience is a plus and working proficiency in English is a must.

Interested candidates should file their pre-application through the official application portal at http://doctoratsindustrials.gencat.cat/en. In order to distinguish the two PhD student positions, we tentatively tagged them `The Syntax Road' and `The Semantics Road', respectively. It is true that indeed one part of the formalization of our mathematics project involves modal calculi whereas another part will emphasize on relational (Kripke) semantics, but choosing at this stage for one of the Syntax or Semantics road does not imply any irreversible decision.

Direct links to the pre-application are
http://doctoratsindustrials.gencat.cat/files/file/attachment/3493/
and
http://doctoratsindustrials.gencat.cat/files/file/attachment/3494/

Upon filing this pre-application, you should send additional information to jjoosten at ub.edu, no later than September 10th, 2016. The additional information should at least contain:
(+) CV;
(+) motivation letter;
(+) transcript of obtained academic results in the relevant master and undergraduate;
(+) e-mail addresses of three references to whom we might refer if needed.

Further information about the positions can be obtained by writing an e-mail to Joost J. Joosten at jjoosten at ub.edu.