- PhD in Mathematics, Computer Science, or a related area

- Proficiency in Coq

- Knowledge of OCaml

- Experience in software design

- Experience in formal verification of software with Coq

- Experience with SSReflect and the Mathematical Components library

Furthermore, the following would be welcome:

- Knowledge of Proof Theory and/or Type Theory

- Knowledge of other proof checkers besides Coq

- Knowledge of other functional languages besides OCaml

- Experience with legal texts

- A strong track record in research publications

The successful applicant will be expected to:

- Conduct cutting-edge research, aiming for constructive interactions with other members of the group. Suggested research areas include (but are not restricted to) proof-theory, type theory, modal logic, ordinal analysis, fragments of first and second order arithmetic, proof assistants, automated theorem provers, and related areas.

- Supervise a team that develops verified legal software

- Supervise PhD students.

We are an active and diverse team, lead by Dr. Joost J. Joosten, which comprises several PhD and Master students with a background in Mathematics and Philosophy, among others. Our group's research involves, but is not limited to: proof theory (pure and applied), provability, interpretability and other modal logics, fragments of first and higher-order arithmetic, algebraic logic, formalized meta-mathematics, and ordinal analysis. We are based in the Philosophy Department of the University of Barcelona, located in the city center of Barcelona. Our PhD students are all enrolled in the doctorate program of mathematics and computer science. Most of us are also affiliated to the Institute of Mathematics of the University of Barcelona and to the Barcelona Graduate School of Mathematics.

In our applied proof theory group we are developing an industrial product with social impact value for the legal infrastructure of transport of people and goods by road. The project is financed by the European Regional Development Fund and the Ministerio de Ciencia, Innovación y Universidades.

Our software is developed using formal methods, with the goal of high reliability in mind. We are using Coq as our main tool.

The working language is English. No knowledge of Spanish or Catalan is necessary.

We offer:

- A competitive salary

- A thriving work environment

- Direction over PhD students

We encourage international applicants who are enthusiastic about formal verification and supervising a team.

Please e-mail your CV to Ana Borges <ana.agvb@gmail.com>, preferably including an expression of interest and relevant background.

We look forward to having you on board!

Ana Borges