coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Chantal Keller <chantal.keller AT wanadoo.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] PhD, postdoc and research engineer positions at Universite Paris-Saclay/Inria
Date: Fri, 22 Nov 2019 12:10:48 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=chantal.keller AT wanadoo.fr; spf=None smtp.mailfrom=chantal.keller AT wanadoo.fr; spf=None smtp.helo=postmaster AT mailext.lri.fr
Ironport-phdr: 9a23:VoDI/RW9KOq+YqonzCr15YEIbHjV8LGtZVwlr6E/grcLSJyIuqrYbBSAt8tkgFKBZ4jH8fUM07OQ7/m7HzVdvd3b6jgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrowjdrNQajIttJ6o+1BfFvGZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+27Ql8JwkblboAq/qBNj347aboaVNP9kcaPce9MRWG5NU8lVWiBEBI63cokBAPcbPetAsYfzp0YAoxiwCwaiC+zg1jBGi2Tq3aA4yektDR3K0QIiEt8IrX/arM/1NKAXUe2t0qTIzS/Mb/VK2Tjn7IjDbxUvru+IXbJ0b8XR01QkGgTZgVWQs4PlOS+V2f4Js2SB7OpvS+avi2o5pAFruTWuyN0jio/TiY0IzVDE8j91wIgvJdChTkNwfNCqEJxVty6ANot2RNsvQ25puCYmyr0GpIW0cDILyJQg3xLfb+aHc4mS7hLtTuacJypzinF9eL+nmhq+70ytxvfhWsS20FtGtDdJn9nWunwQyxDe7NWMROFn8Ue7wzmP0hje6uFaLkAwkqrWM5shzaQxlpoXr0vCETP2lF/yjK+Md0Uo4Oao6/7/brXnoJ+TKZN0hxnjPqgwnsGzG/k0PwoOUmSB5Oix1Kfv8VDlTLlSi/05iKjZsJTUJcQBoa65BhdY3Zoj6xmlCTemzM4XnX0dIFJGZh2Hi4zpNE/UIP3jA/awmVKsny12yPDBOb3tGJvNLmLbnLf7Ybl981JcyBY0zd1H+51UDagBLOvvVU/1qdzXFQQ0Mxe0wubiENVyzJkSWWOJAq+DMaPdq0WE5uw1I7rEWIhAszHkbvMh+vTGjHkjmFZbc7P684EQbSWTHv1gP0ydKVnhhtMMCy9etQo3SvDjjBuBXDpXamyaQKs67z08D8SoF9GQFciWnLWd0XLjTdVtbWdcBwXQQC65JbXBYO8FbWepGuEklzUFUba7TIp4j0OxvQnzx71gaOTOqHVB6cDTkeNt7uiWrikcsCRuBp3HgX6ESWh4mWROSSVkhPki83w48U+K1O1Du9IdFdFX4KoXAAIzNJrR3/A8D8rzHAzbLI+E

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

[Coq-Club] PhD, postdoc and research engineer positions at Universite Paris-Saclay/Inria, Chantal Keller, 11/22/2019