From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC7NZUPX2QPBBHEW53MQKGQEYTJSNXQ@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.6 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-yw0-x23e.google.com (mail-yw0-x23e.google.com [IPv6:2607:f8b0:4002:c05::23e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8987c458 for ; Tue, 3 Jul 2018 14:41:34 +0000 (UTC) Received: by mail-yw0-x23e.google.com with SMTP id l136-v6sf1630753ywb.23 for ; Tue, 03 Jul 2018 07:41:33 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1530628892; cv=pass; d=google.com; s=arc-20160816; b=Lwzhxy/jfbRlNqBZg0KSGL1bJv2Dhq9asVlm29ZBfIGFfb1t29i5KeD8jIHveaFcYF hUO5Os+jagKckWCBS/qrSmqQMMf48WEuXxp3X1x8CBIL+VHzJGQRUdqx+9zJ+CBiKB3g BG+s1KPGUmpBZOrBxDL4kYjI/tyamoDBIq0jUoK0lc4gyaXauOdElzNS8r2sVoi0I4CD Z7YIipw4UQ0t0+Q+yBQExg5OoQn5+B66tAWzlZnVJkOaf+Eu/nnKDdvrQq0LklsZVSGU Vlu8lasJPfR/nVwaPyxzFzBRCakYdx1uaJWdszI3rRtpgnuvWN3ip6muVoq6F6mQTB30 RrGA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:to:subject:message-id:date:from :mime-version:arc-authentication-results:arc-message-signature :sender:dkim-signature:dkim-signature:arc-authentication-results; bh=sE4bAHGRGBlwjqZ3LfWTxtyhSIs2+xDBh2X2Ud4NqdA=; b=FO2XT/AW4+tcw2RjPkqXfCyww+2NuhXnyfChDkPtwAwW6KM5Uj8fiHxTDveEVF6J1I EcLmryX3TYVA/mIQKqsP5t7ipfOUZHQ/JaoBdhyleYIthxypX7zd/H3hSeh7SGWhvnbq NJdPdHvApX/0V5RBtiex8J8jKNhRev6Ve+zYUpVBkqxFw82r9hG7/8fk9wlziugkrfX1 HmPL9UdnryVxMTtzc3EiZwpSkssqZf/+YCTK8Alo373Q4xEORDCcqLQ5j3BRPIjZZFTI mib2T9iTVwoyrz+VeXsrFfMLqG4TIqpMpbboTEupJvYDTxgMS2MxI6maW31FDkT9LQ5u RYEA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=Aih0Si7Z; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4002:c05::244 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=sE4bAHGRGBlwjqZ3LfWTxtyhSIs2+xDBh2X2Ud4NqdA=; b=BiaeEazOIO4Ljx1e4iU7MAMZEAY6ITZfbEJ5FhELBaafWEba8udXFJ1qT8Ab6x3rnr VruJfrB/wmudCOM90ieIbtArPVrvDwyEG8PoDRA0JsN7Q9tk1X5oKtg/4URlKD7+2Jbg hHw9GkNZMEywibzobdR216oiUjtKNKS3gyUpDEBJi7faTkm/xpIDCgXaa2Pc4GajaLIr 3nw/v6+uSzPpf8vouorS+RT5OV2excLJdMFwIxa4T99/LdxdvRWZnxVG/An2hDDa/gBr +aQ1TCyQdCTFLaSAXSjbkzs6T+n3Y5pEStZnUw3DokzP3Fb+cuC2Gvw5eRV3Pt2Z2oFj ZIEA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=sE4bAHGRGBlwjqZ3LfWTxtyhSIs2+xDBh2X2Ud4NqdA=; b=ZqQKA1/I5Rx7sCPPc3AbZccMrkSrTgQzGmHQrMWSKw7cS8ObFHIYuNtbFwt3oRsDeH sqf/uG4ROhVSOCnVtDu5UcPlqE5y1/f251H7/ed2j8T6OZ7rYlsQpGPACyzO+wk1O69h fP6ruTwig1YS1xvhmjl9RR+J+htETAxi3PeOT5L+OGHNSErzJgoqO6+DqXey0CyYtOeJ CF4gA7evfMR8gc04liDYHfjhkMz2uvBHbtxG8DE93BIrCgF9j8HikKHvkX5kYYdkMG/x WVQj/YyqSHlTO8AdWYEr/FETDYFRdy3xOcLOVGJJkDWgjxDlxmqMnuIcCMVgf37UhBS4 dz8w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=sE4bAHGRGBlwjqZ3LfWTxtyhSIs2+xDBh2X2Ud4NqdA=; b=DtwFlSSiHQCNmnA5D1EgTEjdM8KO0hmshfXxo2vdwXiG5QlOFnj9iBQXt3dDnLg+1b 4fwDRqdF3Czpo6bKZ0EWqOQhoGNtJgyNpQohwlFw44ow4bxrJ19qYcTeF5RsJ4UuceCv x6toGZfbMCEaUZ01nJZXToyWf+yLqudJxU2ge9csEIdIS6EtbMmH1eDKosAdYoh3SCy8 XMXNn3/0FTTzzNeMPkA6lJWqqTryK2rpArGur9BSu2elICLJ5NhPMXjjGF/FkPYu1oCC Vlan/SRLaNUNHGEF66mHEMNP4gvjO61mz31R2NiuOahAM4+/uob0vR0C7G99QqYXbL95 oLxw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E1aXLUmt4NqknXZtVTFrMq3iWq654vRYBOyQVSOxo3wEZ5gXyti jdY0S/MJufYebcNtptH7JYk= X-Google-Smtp-Source: AAOMgpf957LAzdpSC3oB832inR9zLytAPttIxTxTtaDpmYyZQNJoo21/S10U3h3SNYrSWVyrSdOPHQ== X-Received: by 2002:a81:9ac4:: with SMTP id r187-v6mr3252311ywg.4.1530628892129; Tue, 03 Jul 2018 07:41:32 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:ce0d:: with SMTP id t13-v6ls127131ywi.27.gmail; Tue, 03 Jul 2018 07:41:31 -0700 (PDT) X-Received: by 2002:a81:3106:: with SMTP id x6-v6mr4265123ywx.189.1530628891820; Tue, 03 Jul 2018 07:41:31 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1530628891; cv=none; d=google.com; s=arc-20160816; b=hhJBzpR/8KbSDrn08Qs/kfaFbwO7e/aKikWcsUYEbCUtRWqI+2ymLZU8oY4YDVq3FG qlNaFlgF8oMTqJv27VKpEt4Z8GVXzT7d4qJxGpzMGQAHMLlKiKmZ6FUUfap3YyiDatGV xd3mVPSPfn30q80selNbFh4odhcnU9X7HJF64Dc7IpZC1bRLO1sv5UrqMwvHuBh93XZL da7JzE1hjU9E5wPkQHXlPVehxlHfalWf2HT/V6yW0x03HhCfPW49dOWecVz34l0CpDbE +tAKo5ciNp0wlRDv/uVQXnvdys7bl8qDxAtgl6+xkBpGa+KtpkQifTB6qaEh9QeSaO/M YUag== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature :arc-authentication-results; bh=aSqCcs35qFaccwEodIqFlDDsx1LCP0HwHeCIx5+jLjc=; b=d+IHXQPPtaWZjBoEFKD8l4Ma1XlX6ShzlAeetSUf442cUDnyuOuEAIfladO7xILhpS 3bjcCuuUbVB0/161GuFAcv8Zh/+C7YYiCPic5HYyc2spk7h6SebYUk58/LlFeHKuML53 85VyxiTQdfKnera8ZjNAUXvZ8e2Bn9b0klZU7QkdmjeOP53lqf9/+ydkvdoLq5BVZjbp h9CtT/CEDXlA7VvgmMqRvwoksD3lOdu/6XTSgFjcLZfYvpkHyITZRLZMeUJOvPTpLQ1N gFphp2WJTR2goKLhRpIZdx2bSpJVRC3bEnzu690m/9YHjdGO2thXAGw5gWCt0YX5F3l+ 965g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=Aih0Si7Z; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4002:c05::244 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-yw0-x244.google.com (mail-yw0-x244.google.com. [2607:f8b0:4002:c05::244]) by gmr-mx.google.com with ESMTPS id r6-v6si75326ybg.0.2018.07.03.07.41.31 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 03 Jul 2018 07:41:31 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4002:c05::244 as permitted sender) client-ip=2607:f8b0:4002:c05::244; Received: by mail-yw0-x244.google.com with SMTP id y203-v6so769230ywd.9; Tue, 03 Jul 2018 07:41:31 -0700 (PDT) X-Received: by 2002:a0d:fec6:: with SMTP id o189-v6mr15251874ywf.195.1530628891560; Tue, 03 Jul 2018 07:41:31 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a0d:c3c6:0:0:0:0:0 with HTTP; Tue, 3 Jul 2018 07:41:11 -0700 (PDT) From: Bas Spitters Date: Tue, 3 Jul 2018 16:41:11 +0200 Message-ID: Subject: [HoTT] PhD/Postdoc vacancy: Homotopy type theory and probabilistic programming To: EasyCrypt Club , fstar-club@lists.gforge.inria.fr, Coq Club , homotopytypetheory , types-announce@lists.seas.upenn.edu, Agda List , lean-user Content-Type: text/plain; charset="UTF-8" X-Original-Sender: b.a.w.spitters@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=Aih0Si7Z; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4002:c05::244 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , 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 -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.