Zulip Chat Archive

Stream: general

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


view this post on Zulip 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

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

view this post on Zulip Gabriel Ebner (Nov 27 2020 at 09:22):

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

view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jason Rute (Nov 27 2020 at 12:52):

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

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip Patrick Massot (Nov 27 2020 at 13:10):

No mathematicians, but lots of computer scientists

view this post on Zulip Patrick Massot (Nov 27 2020 at 13:11):

The dean of our university basically invented inductive types.

view this post on Zulip Patrick Massot (Nov 27 2020 at 13:11):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 13:12):

but it might take a couple of decades :-/

view this post on Zulip 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