From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ed1-x538.google.com (mail-ed1-x538.google.com [IPv6:2a00:1450:4864:20::538]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0c1c913e for ; Mon, 20 May 2019 14:58:33 +0000 (UTC) Received: by mail-ed1-x538.google.com with SMTP id e21sf25605648edr.18 for ; Mon, 20 May 2019 07:58:33 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558364313; cv=pass; d=google.com; s=arc-20160816; b=SefJ8zDfsvvZqur9kV0pezdN0eGfOWq5iDv7Z6dCEiqMtXdFVb1YSAqTtS3g5+eDWj GV+5x1TbbswvgWgklZGc+bPf5d35FBLqr5B8RAebH1KS5MSfCN0yAuuMzoYIZ8slopFl ma7mpfZJe+BSqJu3wsD/kKyDJtQ7qFet6p7sNnVCgRmgMAiaq21G2/ijfsvpVXKjzQDv 5hcha4Alggtj/CNvFLpKwEyas27dNhwPTbVAp9Qfz4k/f/rk38PVVkLUmP3t8eXhfiOt Lm5oq0jFhFWfQQj49uRACnWcGbFK8he0JmksNDqgqPcBAqo4ZlpBv7W9wgDsWArpM7AJ G10Q== 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:content-transfer-encoding:to:subject :message-id:date:from:mime-version:sender:dkim-signature :dkim-signature; bh=Hojh4SDNWbhhq1KMGSY1qLWrGvxLVnsrD1vVjKpmNp0=; b=iSrwYTVXCVw4RrV0h+0jvagCrHI8LskE+fFBiLwtvwA+enD6xKC2DzndHw8ZLpcenI NekEp+F7R4O/fI33V2Qx5SXmwEj25dkOlO2G+sHc9drX1rhGowwqvh8EJsIcpWuLTqyu Wn345uwcRWKXtSbVbB5tcWPuLha+uLxu0msgc0pyWi3NJ8HdomxQmOvmSQaFp0Ov5o9W T7e6FWfntnpHu5l+ClxuEdwMOcaFjyDF7rICvBK2QmuCLB06l74L3VmkFjLPf+PNqs/q D8f4LMKghQoSEnUl9qrFFlFew8L7PYlx8JBvwp7PDgLfD9X29dTwJfUP70fSl4THvQmT sPAQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="C/H8rN4L"; spf=pass (google.com: domain of kaposi.ambrus@gmail.com designates 2a00:1450:4864:20::536 as permitted sender) smtp.mailfrom=kaposi.ambrus@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 :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=Hojh4SDNWbhhq1KMGSY1qLWrGvxLVnsrD1vVjKpmNp0=; b=Kq5MQgA6hrZdotFdJY8bmR1DmmvUw/q++MGf03fs0GbLHi3XuRRWJnasX+EULYhWa1 NXQhGGhu5H7L2hcB8VCSGRGMe/pkmxVoyMRHIsbcwl7l6mmIiYt/ojlPtvE//nEq84OC 8TUL04/rz1Ca4iSFZcBLVHUDfailCSrMmREhbsm40ptLm9TW6w/zrf/iFA5stwhRr997 WsX/urjwVzF2oK5pPSKA1E0VVZExArgz1WLD31exQx3I49FXbeRTSD984KbY4wlXwm5h uSjbE3tGduGeudY6LndGOBMR/yQux0+PrUkem91ibofn4U/M3V7J6I3Pqr+Q+b3TFjxk Mp+Q== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=Hojh4SDNWbhhq1KMGSY1qLWrGvxLVnsrD1vVjKpmNp0=; b=R9PmbNgdjE41aluRtwD1H/49WK/m/zRmnAjuwQ7YpDiO5Dg7t9vuVMR2QLJzEvEcJE WZ9syrjkes7eXdnd57IhpyZ+GJHyhLpi89w+jolyumfMMvuTq5QSLxwvLCenYzU+lY5l 9J0cCyaBATvzQAJ0YFmTB3PsH7hDWirsjXSdvbazXcbh+atJSnYfGMnUZ4i8O5BCNDO8 0tKSp3tlCrHrM+fxOaGL340KxJQ4ERm6H122R8HuKvBCWK/7MoC86HcENvj4P5mnRXgs vydQUvxEHgAhlOGJHg0g4KjClR/hFvFHfluKXsOsULqpPoLeNnbeUOMPRFKr1eXy4SHz JXbg== 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:content-transfer-encoding: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=Hojh4SDNWbhhq1KMGSY1qLWrGvxLVnsrD1vVjKpmNp0=; b=J8DBJWO+mr/RImwvwKSzn4oIDyY/19meoa2C/wUaCtPxZTdBY23y/G9qoQDKDpY2tX rNx+SUkFJflCIhq9qJ7qkkeDZ2iqvYf4UE1q5OZqJx6KjkVBTv9KIViFfsoIEF/u4QUp H+5eOJxeTXkLpXINWHnBjZSPXE1oHUdwSIEoHhBcCu3JE75Ergtr1YVBZ7Qc9fW/rwr9 tu0eE9MkHmLXAbjfVMm1oUFBNP2TwYK5ZC7lDEaq8FzDIo2btmIDwX6fiqqHcMshPrCZ 9UXCqM52iNqznqtJYXRdctq+jSkREXiz9bvD3n9fdUmb1yCaCS8lUFXz5lUkqfiADiPO BraQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAX2/XvH8gd7GA4jCevI+9jXG+aQqRot4L/xsIPHsC951xQUP/bC PYXjgCk7FCXvDiPVvfpNYeQ= X-Google-Smtp-Source: APXvYqwEoAEmHR+N1l8CKm8EXwNosPxCFd8eFSVvASpM+NIU+3grRFWNo0a+IwdWKPP/fZ83h0PDFw== X-Received: by 2002:a50:be03:: with SMTP id a3mr75861790edi.5.1558364312826; Mon, 20 May 2019 07:58:32 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:892b:: with SMTP id e40ls5072629ede.2.gmail; Mon, 20 May 2019 07:58:32 -0700 (PDT) X-Received: by 2002:aa7:d144:: with SMTP id r4mr39478562edo.87.1558364312275; Mon, 20 May 2019 07:58:32 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558364312; cv=none; d=google.com; s=arc-20160816; b=iFcpe3QXZge8KMmS5hI/p/PiAsmvUGDLCuQKs3YDsNE/xmR7c9VIJn2jivwxgVwXoV h6wX50MeF4PosE80wsXYFp1VujNmuSf27tj2wgqJbPuJ/NuOcQHi9VktR6jLfKEM7l7K bLhNKB/xEIBXJytFVYqI2pZdevJ1PUvOnUN8XQaRqAAl+4TrVMjT6bc3kqgP9leWx4Bw IM59f4bvd6iXk7V1CGalyQ+VI5DCZWvzPWHS5uGu0PjJZuL+2LSfsSK+LYzHeEiidMYV 9PtCRms+tzQ3YLATJCD+Y6IsBUGYn240XFVER2Y4cjczcJQ0Sq7RIokrKEzN0GuXWKv9 iXYg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :mime-version:dkim-signature; bh=QIl7OCUyyrn2XwKtcCyaI/iv8LXty85YUbdFD/T/jZY=; b=K9WdQ0RCjHHZOZ7LY42OMjmqLcRMnnVG4Y9hwP2Fnrrp7OQTMv+JsbFkQe8wjRmo6A A6yrq9PPV8XHAT7iQzWMjAPjAkjkn6duEU7rLPQwPrXbXijgtm1PrdjBk0AaJe+Qm64o zeoAH/aNCXUcCMF91OMCRUzR2eXyp7Ea1f9q+b2lHVQjRhOwciviC6W22OJkl91WtLzs O8eY2NG+zA5OdLvUzu60B2y+pKfYzuranPDGzo0s/uiwp3dkp6em5eiPMFOfpDP4cu4o pfw6Yvaa/B4quYM2Ag9hkWrEzmlybr6dHqVUMtaeFxuTRxQ0jzAd8NUGT439W3sNiAbk qDnQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="C/H8rN4L"; spf=pass (google.com: domain of kaposi.ambrus@gmail.com designates 2a00:1450:4864:20::536 as permitted sender) smtp.mailfrom=kaposi.ambrus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ed1-x536.google.com (mail-ed1-x536.google.com. [2a00:1450:4864:20::536]) by gmr-mx.google.com with ESMTPS id z45si2089104edc.3.2019.05.20.07.58.32 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 20 May 2019 07:58:32 -0700 (PDT) Received-SPF: pass (google.com: domain of kaposi.ambrus@gmail.com designates 2a00:1450:4864:20::536 as permitted sender) client-ip=2a00:1450:4864:20::536; Received: by mail-ed1-x536.google.com with SMTP id a8so24352374edx.3 for ; Mon, 20 May 2019 07:58:32 -0700 (PDT) X-Received: by 2002:a50:f48d:: with SMTP id s13mr76821949edm.151.1558364312093; Mon, 20 May 2019 07:58:32 -0700 (PDT) MIME-Version: 1.0 From: Ambrus Kaposi Date: Mon, 20 May 2019 16:58:20 +0200 Message-ID: Subject: [HoTT] PhD studentship in Budapest To: agda@lists.chalmers.se, coq-club@inria.fr, homotopytypetheory@googlegroups.com, types-announce@lists.seas.upenn.edu Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: kaposi.ambrus@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="C/H8rN4L"; spf=pass (google.com: domain of kaposi.ambrus@gmail.com designates 2a00:1450:4864:20::536 as permitted sender) smtp.mailfrom=kaposi.ambrus@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: , Dear All, The Faculty of Computer Science at E=C3=B6tv=C3=B6s Lor=C3=A1nd University = is advertising a PhD position in type theory. The prospective student would work together with Ambrus Kaposi and Andr=C3=A1s Kov=C3=A1cs. PhD scholarship is 300thousand HUF net a month and the PhD programme lasts 4 years. The deadline for applications is 31 May. The application process is described here: https://www.inf.elte.hu/en/content/application-process.t.1834 If you are interested or know someone who is interested, please contact me directly as well. Students interested in other topics are also welcome, here is the full list of advertised topics of the Faculty of Informatics: https://doktori.hu/index.php?menuid=3D116&num=3D22&lang=3DEN Best wishes, Ambrus Kaposi Department of Programming Languages and Compilers Faculty of Informatics E=C3=B6tv=C3=B6s Lor=C3=A1nd University Budapest, Hungary --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CACSS4jn5y7iRhDTUP44DxwtEx4x1HMQ%2B_e_pmXDqkNRVLfhguw%40= mail.gmail.com. For more options, visit https://groups.google.com/d/optout.