[TYPES/announce] PhD Position in logic and formal verification

[Ana Borges]

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_UB_PE6_PE1_20190701.pdf


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 vacancies at formalvindications.com.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20190701/c47e0691/attachment.html>