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=-0.9 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-wr1-x437.google.com (mail-wr1-x437.google.com [IPv6:2a00:1450:4864:20::437]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 45f325eb for ; Fri, 25 Oct 2019 07:27:20 +0000 (UTC) Received: by mail-wr1-x437.google.com with SMTP id j14sf584154wrm.6 for ; Fri, 25 Oct 2019 00:27:20 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1571988439; cv=pass; d=google.com; s=arc-20160816; b=eLEEd2ViqGPddKLvKj3BOEPyVkExCSX0Yu0+FY3DzpFUN/qDvXoAGsfPhXYQ2OwdrY VGNfDqwm21VczrAXPxUtnsNkTbLAMxmc8BBVq4T6cRCTQE9sr2MYCkHR2yZlGNQ1Z21Y JXLjYg6lqSSDeojCnQd4WiyerAudXjmLsfj+5D4OwpUHEzGtkIKbBDhAPQQQws/yBaUR COpJ4yneKOvFNKnDuACQYY6HuV8k/vlI4hdOmmUN9cpl8kLSOoMRUhHk1fVr98C0uHnY v8hQJlHRub0BqOQQN/4zdLYmv/YhuNmTd+m2vkHX42KMg3kMjXcV7DcopWIQIBWIIlIb u+gQ== 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:mime-version :message-id:subject:to:from:date:sender:dkim-signature :dkim-signature; bh=DAuavZbcjLDToAVBC3XnzbWLIBiTz4xbF6NJbY5Ulqg=; b=tT+b6WzJMrAPUMQO58F90Rw6S8u5I4QOSs1Uhc8HHtjQ9wHF5IZG17VN2ZgvXeOHxt ei3cQOP+hzpmmAkMHPNcVG/TUWsyxwNXzZDxbXPTKniayHuk9go77I+TGK426nEQe0H6 mTs9zyflBnAjiE11Cp0d0lfQZsYUhuvDQIvd8AUUiM9OOxm6I9L/BVfCtM5OvtnqrWRa L1yvr8LrKGVIbki+2itVQe39LzOheFKajpTIakLKmYFZBIw5SkOsti1+G7DDYBvl+xu1 6Ny7mAtwZnxJLzJpxJL8etOuuSQ5XN66T33ojbVigsvobrO0tiSTGoTyEPDX/864IbeI blgQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="a3z2O7X/"; spf=pass (google.com: domain of ichor88@gmail.com designates 2a00:1450:4864:20::129 as permitted sender) smtp.mailfrom=ichor88@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:date:from:to:subject:message-id:mime-version :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=DAuavZbcjLDToAVBC3XnzbWLIBiTz4xbF6NJbY5Ulqg=; b=Ulu84AYWAQCtdgXL8vnzKGK4+1IuK/hjObT6kBO+hn1255Hui3lis6ObrQFVkntRnG Lt1TDTml2nOnDI+Vhc2/QXtXZZ0r1wSARMNGGYMP6vzw4g3MUUUlKhXTdunmDUYdXKg+ mvt+Jer0UTFG9CmqmEeTyA4C6j6DELi7g9/nOSEBo+FQ/thXmiU4cXbOAAPVJowxmjwR zRa+/73wq1DH0zCSuVya6ZhTnWr0v77p7zXMB5SDikdjI4/TYAckl/PCTeHop0PN4NHd 7QqnEjS3wQbpl3GDEybIMJrtC0vZO2s4lJSalWZJHN3DQLnlckJtNvNfUe6FxunS4kEP vwtg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:subject:message-id:mime-version :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=DAuavZbcjLDToAVBC3XnzbWLIBiTz4xbF6NJbY5Ulqg=; b=DNQ7a3AcaFLmLlyJlkkuNT+DW0azZ5GWnPAG4cxH2pogsuQHyg3hvR7lrP+xyirk42 nDSfkpaDPdXesIUV+VZLPi1kJGrAaLcM8Xi4TghTw4A5/SVvQ7C7bWrgMYdHEHRpz2+W E4KJ9jXZx0C093JSia7KqEC/bBcKB9KfyT4ypXOetvS2dydNTxCd3AtjPcw7umb78IRW TiFh1PSxEgHG/FuxPIx/YWIxv0i3G4Q7EytcXt3+tdsxkhJqRl5v5TzqsfTXH52+e9aH omxTjUKv3+TDoF1JS4cNc9aWW3xOQQVWFMNxmF2xz5e4vJrYBbeMZY5uzEZt0sOUunIC 7PTQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:subject:message-id :mime-version: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=DAuavZbcjLDToAVBC3XnzbWLIBiTz4xbF6NJbY5Ulqg=; b=JpsYMSOj4EjkBaGYbWwZyYsEKftaRzAVfBA5okgLeZNblu7MP0jJynRj3sEGhCi5Q8 JWXY+IRvKWgGkSmtvVYK7xzXXpy+LOx5s75kX8L1Ln+2pbXYYavcsmPxy+qszp5jjBxF DFoaxn+zTqwpE9z7KEYFcsu/+VJ2gM5kYjhyrJNtJ494kpBqOIKrGvpRnE6HL76pSOEI q58DahLI8YoBL+OjoDphHwH1oVkW4fLM3ptkYoAQtLOjArc9YhXmORp8nCdnNr/Up2gY TISgpLwLUmVb26z774krPh4Ox9QwXXr40NqEHHWatGmTsgSzcjpsjNNPy9c9IeKybihl 0qYQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVFu34i3lzREfakf5lzW7cwJ2A0i7fz1H0PxKRX9JUqAZtE5ZgZ 17JlTNpXPawwjRRt3ao/wXs= X-Google-Smtp-Source: APXvYqyBcRlqmX9dthmNmSjXmJhAaT7A8mFEpgPSCbe7fpf5PWqt4bP0M3PJrBDt1nElVMF8glXQ8A== X-Received: by 2002:a7b:cf30:: with SMTP id m16mr2067984wmg.89.1571988439843; Fri, 25 Oct 2019 00:27:19 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6000:12ca:: with SMTP id l10ls4951926wrx.16.gmail; Fri, 25 Oct 2019 00:27:19 -0700 (PDT) X-Received: by 2002:adf:f4cb:: with SMTP id h11mr1602490wrp.260.1571988439320; Fri, 25 Oct 2019 00:27:19 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1571988439; cv=none; d=google.com; s=arc-20160816; b=Wuxio0w1ikDMKmTlCv1oMU7AqCMdNkodI2SFdZeicXrmcIFR7H/s3c5EgOMWerQ0qe cqs0wmpG7ONlOWILLJMOBAB+8OmErs6cZ2tBISiuacP6GiZSCkmgaRq+d4t9XnBJTPAf 4nlSwxaY5MqDfZ7ZrHJi3pgTMuGZfpewlyvLIcFUAmRtjOYEh392gSuSt7BN2xE3KZwG jKHMwRDHTPmhOEsbwIVvG5oI/Kq7HtcgxEq7eYVuGrF9aDsuHvMM5bzmrq8Egd8Efp7I CyUKFEERLj8FysaI60y7b0/GKI6juoiE9zr8haz+/vCnD9bLdlkpu/1bmcIlOlmVZRIJ zfGg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:mime-version:message-id:subject:to:from :date:dkim-signature; bh=j4aHIG+VXFSS2GQExeGA9SVaNRt2LfWmkWaE10UzZ5o=; b=WALMKG7gy7aLDfBw1pT6ygu7XdcGV8+YmO9jZEBGnavoCrvJnI6wDb9E0IvahzJDES OOuKlW6DB05+JUsrN4HY69VXMyPrXo0eTjUpcKlEgcjOUv1GVQkl1sV7jzucZcrcQ2Ho Hs5yIIrpkMBLuLnWFxSoHFtey6nCe8MaOUwHQfQcZpF+H25lCp/Qb30PjKJq59diiIfQ d4JLMXqiCxHUT4UUnbZ2QoUGVNoBXRusVnMHMEeinYcN6NlNz0jwQowk+tUBcD80ii1Y spuY96GrS8rrbTEGTyuO4EvrcZusKu/oobHVSqSxB1vEa1VfaYswDTwg2oNGxfn55weu p9Ng== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="a3z2O7X/"; spf=pass (google.com: domain of ichor88@gmail.com designates 2a00:1450:4864:20::129 as permitted sender) smtp.mailfrom=ichor88@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lf1-x129.google.com (mail-lf1-x129.google.com. [2a00:1450:4864:20::129]) by gmr-mx.google.com with ESMTPS id y188si69854wmc.0.2019.10.25.00.27.19 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 25 Oct 2019 00:27:19 -0700 (PDT) Received-SPF: pass (google.com: domain of ichor88@gmail.com designates 2a00:1450:4864:20::129 as permitted sender) client-ip=2a00:1450:4864:20::129; Received: by mail-lf1-x129.google.com with SMTP id y127so879831lfc.0 for ; Fri, 25 Oct 2019 00:27:19 -0700 (PDT) X-Received: by 2002:a19:ca13:: with SMTP id a19mr1471245lfg.133.1571988438829; Fri, 25 Oct 2019 00:27:18 -0700 (PDT) Received: from gandalf.openbastille.org (15.79-161-119.customer.lyse.net. [79.161.119.15]) by smtp.gmail.com with ESMTPSA id t10sm431203lfq.13.2019.10.25.00.27.17 (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Fri, 25 Oct 2019 00:27:17 -0700 (PDT) Date: Fri, 25 Oct 2019 09:27:16 +0200 From: =?UTF-8?B?SMOla29u?= Robbestad Gylterud To: agda@lists.chalmers.se, homotopytypetheory@googlegroups.com, types-announce@lists.seas.upenn.edu Subject: [HoTT] PhD position in type theory at the University of Bergen Message-Id: <20191025092716.a6778bbfa43dde229962035c@gmail.com> X-Mailer: Sylpheed 3.7.0 (GTK+ 2.24.32; x86_64-unknown-openbsd6.5) Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: ichor88@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="a3z2O7X/"; spf=pass (google.com: domain of ichor88@gmail.com designates 2a00:1450:4864:20::129 as permitted sender) smtp.mailfrom=ichor88@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, There is a PhD position in type theory (fully paid, 4 years, 25% teaching) available at the Department of Informatics, University of Bergen, Norway. Possible directions include homotopy type theory, applications of type theory to computer science or computerised formalisation of mathematics. Details can be found on the link below. Notice the short application deadline (November 15th 2019). If you have any questions, you can contact H=C3=A5kon R. Gylterud, hakon.gylterud@uib.no. https://www.jobbnorge.no/en/available-jobs/job/177230/phd-position-in-infor= matics-type-theory Best regards, =E2=80=94H=C3=A5kon R. Gylterud --=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/20191025092716.a6778bbfa43dde229962035c%40gmail.com.