coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] PhD/Postdoc vacancy: Homotopy type theory and probabilistic programming

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: EasyCrypt Club <easycrypt-club AT lists.gforge.inria.fr>, fstar-club AT lists.gforge.inria.fr, Coq Club <coq-club AT inria.fr>, homotopytypetheory <homotopytypetheory AT googlegroups.com>, types-announce AT lists.seas.upenn.edu, Agda List <agda AT lists.chalmers.se>, lean-user <lean-user AT googlegroups.com>
Subject: [Coq-Club] PhD/Postdoc vacancy: Homotopy type theory and probabilistic programming
Date: Tue, 3 Jul 2018 16:41:11 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f195.google.com
Ironport-phdr: 9a23:Jj0WpRXuGBX3+IF7pxPr51z0OxDV8LGtZVwlr6E/grcLSJyIuqrYZRSOvKdThVPEFb/W9+hDw7KP9fy4BypYud6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9uLRi6txndutULioZ+N6g9zQfErGFVcOpM32NoIlyTnxf45siu+ZNo7jpdtfE8+cNeSKv2Z6s3Q6BWAzQgKGA1+dbktQLfQguV53sTSXsZnxxVCAXY9h76X5Pxsizntuph3SSRIMP7QawoVTmk8qxmUwHjhjsZODEl8WHXks1wg7xdoBK9vBx03orYbJiIOPZiYq/ReNUXTndDUMlMTSxMGoOyYYUMAeQcI+hXs5Lwp0cSoRakGQWgGP/jxz1Oi3Tr3aM6yeMhEQTe0QE9Bd0Oq2nfosjtNKcTTeC10LfHzS/Yb/hL3jry85LEfQo7rfCCR75watLRyUgzFwPZkFqQs5flMiia1uQIqWeb7u5gWfizhG4grgF8uz6izdoihInOg4Ia0FHE9SNhzYkvP925R097YcC+HJtXrSGaOJN6QsI4TG50oiY20LoGuYS0fCQS0psn2gTTZOGEc4WO/xntV/6RLC9miH55fL+znRW//Ei6xuHhV8S4zUxGojdBn9TMsH0Gygbd5dKdSvRn+0eswTaP2B7X6uFDOU00kLDUK58lwrIplpsSv1jPEjb4mEnriKKbdl8o+uev6+TgbbXmooGTO5VohQH5N6Qigs2/AeImPQgSR2WX5/iw2bn58UD6QLhGlOA6n6jEvJzAOMgWoq60DxdQ0ok56ha/Czmm0M4fnXkCNF9KYwiLgJLzN1DAOvz4Fu+/g1WwkDd32f/GJKbhD47CLnjGirjhfLJ951RAxwo0yNBT/4hUBa0ZIPLvRk/xs8TVAQM+Mwyt2uroFNF91p4FVm+UGa+YMKbSsUeS6e41IumMYpUVuDfnJPQ/6f7ulyxxpVhIUKCyzLANeWikVt9iPk/RNXflmcYKC3YSok81SPHgoFmDSiJIIXm8WLgz63c6DpinBMHNXNbpyLKawC6hW5ZSe2puDlGXDWyueIuDQfgBLiOUOM5o1DIeEfCKTJZp/hWzvkeuwL1+a+HQ5ycwtJT51dEz6feF0Vky8jlzE8OFwn2cV2xonm4PXS5+iKB4pEthzU+SzblgjuBYGNtJ9ttGVQA1MZPT1etnE8u0UQXEKJPBVEe+T87jCDc3Sc83yNImZ0dmB87klR3KxGy3G7ITkfqGCIFwuovT03G5A8dm1z6S3aYthnEiQ9BTLiuthqd78gXJHMjSnhPd36KnfKJZwTXA7i/XyWeHugRFSwNqearCWn8ba0TMqsnh/QXJSLr4Wpo9NQ4U48eZYpBSa8H1gE9dDKPpft2YfCSqg2asGRuS3ZuDaYPrfyMW2yCLWxtMqBwa4XvTbVt2PSymuW+LSWU2TQu+MXOpyvF3rTaAdmFxygiLa0N70L/so0wagPWdT7UY2bdW4X59+QUxJ0602pftM/TFvxBoJfwObtY04VMB3mXc5VQkY86Qapt6j1tbSDxZ+kPj0xItVNdFmMku6WI1lE98cPPFllxGcDyc0Nb7PbiFcmQ=

Aarhus University in Denmark has a PhD and a postdoc vacancy on the
AFOSR funded project:

Homotopy type theory and probabilistic programming

The goal of the project is to use type theory for probabilistic
programming and computer aided proofs in security.

Postdoc:
http://cs.au.dk/about-us/vacancies/scientific-positions/stillinger/Vacancy/show/985804/5283/
Application deadline: 12 august 2018.

PhD:
http://talent.au.dk/phd/scienceandtechnology/opencalls/calls-on-specific-projects/august-2018/type-theory-probabilistic-computation-and-computer-aided-cryptography-proofs/
Application deadline 1 August 2018 at 11.59 PM MET

Related publications include:
* Florian Faissole and Bas Spitters, Synthetic topology in Homotopy
Type Theory for probabilistic programming
http://www.cs.au.dk/~spitters/ProbProg.pdf
* Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters,
Pierre-Yves Strub, Computer-aided proofs for multiparty computation
with active security, CSF https://eprint.iacr.org/2018/502
* Daniel Huang, Greg Morrisett, Bas Spitters, An Application of
Computable Distributions to the Semantics of Probabilistic Programs,
https://arxiv.org/abs/1806.07966

[Coq-Club] PhD/Postdoc vacancy: Homotopy type theory and probabilistic programming, Bas Spitters, 07/03/2018