[Agda] PhD, postdoc and research engineer positions at Universite Paris-Saclay/Inria

[Chantal Keller]

Hi

We are looking for a PhD student, a 2-years postdoc and a 2-years
research engineer to work on automatic theorem proving in Coq and its
application to blockchain verification.

The first objective is the development of SMTCoq
<https://smtcoq.github.io>, a plugin to safely enjoy automatic theorem
proving inside Coq. In collaboration with the Nomadic Labs company, a
second objective is the application of proof automation to the
verification of the Tezos blockchain.

The detailed description of the positions can be found here:
<https://www.lri.fr/~keller/positions-en.html>. The positions can start
quickly.

Please contact Chantal Keller <Chantal.Keller at lri.fr> and Valentin Blot
<research at valentinblot.org> if you are interested or if you have any
questions.

Chantal