[HoTT] Fwd: Job opening: post-doctoral research and development position at the University of Barcelona

[Ana <ana.agvb@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 3156 bytes --]

We are looking for a senior researcher and project manager who has (a
significant subset of) the following:
- 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

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 3874 bytes --]