Descripció del projecte
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. In particular, the applicant can propose to work on Coq-related question for the PhD research and propose an external PhD supervisor for that.
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 five years of experience with proof assistants, type-theory and pure and applied proof theory. There are three 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 is realistic expectations that the PhD will be finished soon, the company will continue 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 are at least 2200€ per year and the gross salary varies is around 22K per year which is well above average for Spanish standards.
We are looking for very storng 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/highly recommended 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. After a first selection, candidates will be asked to file their application package no later than September 5.
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.
