Logic List Mailing Archive
PhD student position on formal verification of legal software, Barcelona (Spain), Deadline: 5 Sep 2019
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
(https://urldefense.proofpoint.com/v2/url?u=http-3A__formalvindications.com_&d=DwIFaQ&c=slrrB7dE8n7gBJbeO0g-IQ&r=xXZM6ZrkjVxXknjzIxhAvQ&m=ANK0tuSKCafJLpsjnBU-NNU_b_mTBqDoy6OJqFK8UQw&s=KRsedriQU-z6DTE_NZvs1H09OAt0p7bEM37j53s-9pk&e=
). 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:
https://urldefense.proofpoint.com/v2/url?u=http-3A__doctoratsindustrials.gencat.cat_files_file_attachment_7019_072-5FDI-5FFV-5FUB-5FPE6-5FPE1-5F20190701.pdf&d=DwIFaQ&c=slrrB7dE8n7gBJbeO0g-IQ&r=xXZM6ZrkjVxXknjzIxhAvQ&m=ANK0tuSKCafJLpsjnBU-NNU_b_mTBqDoy6OJqFK8UQw&s=YkH2kL09ur6IMlXYeeuVGvR96z9LPPGN3k32IzSm9IM&e=
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@formalvindications.com.
--
[LOGIC] mailing list
http://www.dvmlg.de/mailingliste.html
Archive: http://www.illc.uva.nl/LogicList/
provided by a collaboration of the DVMLG, the Maths Departments in Bonn and Hamburg, and the ILLC at the Universiteit van Amsterdam