The Coq mailing list

[Ana Borges <ana.agvb AT gmail.com>]

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 (http://formalvindications.com/). This work will be complemented with the formalization of parts of logic/mathematics. 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. Currently, the group is lead by Joost J. Joosten and consists of three researchers who have over two years of experience with proof assistants, type-theory and pure and applied proof theory. There are two fellow PhD students working on related topics. Furthermore, the project counts with three junior scientific staff members, a senior Coq developer and a versatile programmer. The group is embedded into various research projects, including European, National and Regional funds. The general logic landscape of the Barcelona metropolitan area is rich and diverse and counts with groups and specialists in areas like algebraic logic, computability theory, formal linguistics, model theory, and set theory.

We offer a three-year position in the PhD program in Mathematics and Computer Science which is located in the very center of Barcelona. If after three years the PhD has not been finished, but there are 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. The travel allowances can exceed 2200€ per year and the gross salary varies between 18K and 22K per year depending on how much financial support this project receives from the Catalan authorities.

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 undergraduate and master score of at least 6.5 out of 10. 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 make their first statement of interest through the official AGAUR site, where they can fill in a pre-application. A direct link to it is:
http://doctoratsindustrials.gencat.cat/files/file/attachment/7369/097_DI_FORMAL_VINDICATIONS_UB_PE6_PE1_20191028.pdf


After a first selection, candidates will be asked to file their application package no later than November 15. The application package should contain:

(+) CV;
(+) Motivation letter;
(+) Transcript of obtained academic results in the relevant master and undergraduate;
(+) Email addresses of three references to whom we might refer in case we consider this desirable.

Further information about the position can be obtained by writing an email to Aleix Solé at vacancies AT formalvindications.com.