The Coq mailing list

["Joost J. Joosten" <jjoosten AT ub.edu>]

PhD student position on proof theory and verification of legal software, Barcelona, Deadline: April 3th, 2022 (AoE)

The University of Barcelona offers a 3 year 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 (formalvindications.com). This work will be complemented with the formalisation of parts of logic/mathematics and possibly research of a less applied nature.

As such, there are two possible tracks:

(1) The PhD student proposes an external supervisor with whom to work on academic Coq-related questions (such as verified extraction, or others);

(2) The PhD student works under the supervision of Joost J. Joosten (joostjjoosten.nl) in the area of proof theory and formal logic for the academic part of the thesis.

Gross salary is about 22K€ per year (well above average for a PhD student in Spain) and comes with a travel allowance of at least 2200€ per year. Starting date should be around August/September 2022.

The successful candidate will enter an active and strong logic group in Barcelona. They will be trained on Coq and functional programming in OCaml by an experienced team. If needed, the contract can be extended after the initial three years.

We are looking for very strong candidates with a background in theoretical computer science, mathematics and/or mathematical logic. It is a strict requirement to have finished a relevant Master degree with an average undergraduate and master score of at least 6.5 out of 10.

Interested candidates should send their CV, letter of motivation and academic track record to Aleix Solé <aleix.sole AT ub.edu>.

Further questions on the position can be sent to Joost J. Joosten <jjoosten AT ub.edu>.

Joost J. Joosten

University of Barcelona

C. Montalegre 6

08001 Barcelona, Catalonia, Spain

Office phone: +34 9340 37984

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.