Research position in applied proof theory, Barcelona (Spain)

We are looking for a full-time Mathematician or Computer Scientist researcher to participate in a 3,5 year project. 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.

Our software is developed using formal methods, with the goal of high reliability in mind. We are using Coq as our main tool. The successful applicant will be expected to have proven experience with Ocaml or similar, as wel as LaTeX.

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.