Postdoc positions in AITP, deadline Dec 3, 2020

Stream: general

[Vasily Pestun]

Two postdoc positions in automatic and interactive theorem proving in dependent type theory (we are using Coq currently) will be opened with a starting date September 1, 2021 at IHES, France

See details and apply before the deadline December 3, 2020

ihes.fr/en/applications/post-docs/huawei-young-talents-programme
ihes.fr/en/applications/post-docs/ibm-postdoctoral-position-in-artificial-intelligence

[Gabriel Ebner]

The links are missing the www. in front, BTW.

[Jason Rute]

https://www.ihes.fr/en/applications/post-docs/huawei-young-talents-programme/

https://www.ihes.fr/en/applications/post-docs/ibm-postdoctoral-position-in-artificial-intelligence/

[Patrick Massot]

@Vasily Pestun nice! Someone posted a link to the CertRL paper a few days ago but I assumed, without even thinking about it, that it was from an another Vasily Pestun. I had no idea you were interested in formalized mathematics and programming (although I knew Coquand was meant to visit IHES last spring, he asked me to give a talk during a workshop that was cancelled because of Covid). It would be really nice to have formalized mathematics in IHES.

[Patrick Massot]

For people that are unfamiliar with French mathematical geography, IHES is within walking distance from my office in Orsay.

[Jason Rute]

Here is the CertRL paper: https://arxiv.org/abs/2009.11403

[Patrick Massot]

And of course IHES is an extremely nice and quiet place. From there you can also easily access people using Coq in Orsay or École polytechnique, and all of the Paris area in general.

[Anatole Dedecker]

Patrick Massot said:

And of course IHES is an extremely nice and quiet place. From there you can also easily access people using Coq in Orsay or École polytechnique, and all of the Paris area in general.

Are there a lot of Coq users in Orsay ? Mostly mathematicians or computer scientists ?

[Patrick Massot]

No mathematicians, but lots of computer scientists

[Patrick Massot]

The dean of our university basically invented inductive types.

[Patrick Massot]

(this is probably a ridiculous over-simplification, but still)

[Kevin Buzzard]

Also, the trick which the computer scientists realised is that if you teach the undergraduates about theorem provers then you end up with users of theorem provers

[Kevin Buzzard]

but it might take a couple of decades :-/

[Patrick Massot]

https://en.wikipedia.org/wiki/Christine_Paulin-Mohring