## Stream: general

### Topic: Postdoc positions in AITP, deadline Dec 3, 2020

#### Vasily Pestun (Nov 27 2020 at 00:00):

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

#### Gabriel Ebner (Nov 27 2020 at 09:22):

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

#### Jason Rute (Nov 27 2020 at 12:30):

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 (Nov 27 2020 at 12:45):

@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 (Nov 27 2020 at 12:46):

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

#### Jason Rute (Nov 27 2020 at 12:52):

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

#### Patrick Massot (Nov 27 2020 at 12:56):

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 (Nov 27 2020 at 13:06):

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 (Nov 27 2020 at 13:10):

No mathematicians, but lots of computer scientists

#### Patrick Massot (Nov 27 2020 at 13:11):

The dean of our university basically invented inductive types.

#### Patrick Massot (Nov 27 2020 at 13:11):

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

#### Kevin Buzzard (Nov 27 2020 at 13:11):

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 (Nov 27 2020 at 13:12):

but it might take a couple of decades :-/

#### Patrick Massot (Nov 27 2020 at 13:20):

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

Last updated: May 11 2021 at 21:10 UTC