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 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 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/7019/072_DI_FV_...

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.

Further information about the position can be obtained by writing an email to Aleix Solé at [email protected]mailto:[email protected].

Aquest missatge, i els fitxers adjunts que hi pugui haver, pot contenir informació confidencial o protegida legalment i s’adreça exclusivament a la persona o entitat destinatària. Si no consteu com a destinatari final o no teniu l’encàrrec de rebre’l, no esteu autoritzat a llegir-lo, retenir-lo, modificar-lo, distribuir-lo, copiar-lo ni a revelar-ne el contingut. Si l’heu rebut per error, informeu-ne el remitent i elimineu del sistema tant el missatge com els fitxers adjunts que hi pugui haver.

Este mensaje, y los ficheros adjuntos que pueda incluir, puede contener información confidencial o legalmente protegida y está exclusivamente dirigido a la persona o entidad destinataria. Si usted no consta como destinatario final ni es la persona encargada de recibirlo, no está autorizado a leerlo, retenerlo, modificarlo, distribuirlo o copiarlo, ni a revelar su contenido. Si lo ha recibido por error, informe de ello al remitente y elimine del sistema tanto el mensaje como los ficheros adjuntos que pueda contener.

This email message and any attachments it carries may contain confidential or legally protected material and are intended solely for the individual or organization to whom they are addressed. If you are not the intended recipient of this message or the person responsible for processing it, then you are not authorized to read, save, modify, send, copy or disclose any part of it. If you have received the message by mistake, please inform the sender of this and eliminate the message and any attachments it carries from your account.