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-lf1-x140.google.com (mail-lf1-x140.google.com [IPv6:2a00:1450:4864:20::140]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 11229557 for ; Sun, 13 Oct 2019 11:57:12 +0000 (UTC) Received: by mail-lf1-x140.google.com with SMTP id x20sf2553465lfe.14 for ; Sun, 13 Oct 2019 04:57:12 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1570967831; cv=pass; d=google.com; s=arc-20160816; b=XIavm/Pf/GF2gVVUNAwIwg9p3PWgUktPEq2PB+M1jsJAjxRTmxIv2+GfPFbLaLNTxe Vl3ibEOwbbrWCpjPoggB3HJRe66tOiEWCMQk3naQEYR0q8g4pGUbj50DSNiWN+8zuK50 VYyOezhtW/A0BC6F4kudklALLm85isS9XiUoZTZZ7BnIvciIKReoUg1PPOAygGzToKdw ntoXI1k5QPQ84Zj8a65jNAcYxk+xBpEnFejKZXlG40ZK5KDBBY70T/0LLEv/pyT52TqH KZySvQT+cuRtiNXTOPt6YIBNZ/qoKGNHd3K1ZXpyntfZLXKpJ635CKW3zczLJZZTCm5T dkLQ== 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-language:mime-version:user-agent :date:message-id:to:subject:from:sender:dkim-signature :dkim-signature; bh=rReW1k5GAVJgbNG0UixYUkFg5DmtnjLlfqHFNtL/8e4=; b=b212iOp5U/ukUfPedNz+iTagwPa6d/RdnuEbLeXEzAH+GHSQjTTPxavQFiV4qJ4X4k AUebHUUY548RCR4I2KVk0qvhN3eX2k4/BS5ujMf44kVm/8qrtT3gcuJqm+uAAdpGE/LM nxHvfucnWg6Z4DRfkrS079wgTPANIlhktvtLRkGJxlKmxQqu8GNMiZuqt8qpo/EGiunq 5tTH1v8cccot25autLJYy5B/PQyHvajNeWJ9QgyucENfu2LGFzNECf5epvx+RekE8wOh 9XQQXoADdRQPawVKP/1LvWxObOVQuAw5lMHxreakiAmsdYYYIa7DbHVpk12o/CAtvdIv fWSg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=q8USC7wR; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::334 as permitted sender) smtp.mailfrom=benedikt.ahrens@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:from:subject:to:message-id:date:user-agent:mime-version :content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=rReW1k5GAVJgbNG0UixYUkFg5DmtnjLlfqHFNtL/8e4=; b=U1EgaJ7zXdFYw4GaXDSfbPyW6lZf9vCe0jq3rNuysobSlRqcgrmRuQ38b8TBCJDT9e ytGLtcPnC/djgJ+2/jIjnpWwQ92fssHOHTfhFhb4uh08uWV0SMqVeiYrXbKY03IX0JM7 pP8UM3j2xb0I9jRlfAmHgSndZnbHmssUBwtdOJI4I7LKp5ItWNki6bWkFSNRYltaR+UM 9zwlfSXZHRESQOgYlPRR1X9rmCIOES7agaGDN6qFhSfW52meb7ufHUTD2xAHWtTtI7Av aglgJUeTZ2mAy11/LqrAS6L+WVgqsfXJbVCRM7qMcxc8g6GQyBC8WaGJDOUx9qsZYNqm ApOg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:subject:to:message-id:date:user-agent:mime-version :content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=rReW1k5GAVJgbNG0UixYUkFg5DmtnjLlfqHFNtL/8e4=; b=QiWTO8M4PpVMdDkJg9LJnOW/YHVPpQfbEly8fgX54kBi88rHOPVZnIB9nt7XLXgrmc ElKMlbwA3O+pJl3qfpsxR2QJEch6dkFX4R1S98T1o1abGknLoZesWrso3W7fvzaUzlqY TRJe1YmcM0Z1cSBw/laCNVpm9sHYCoVGbFHNujSIuc2YIisctmM3bVunn34E58E7wTFc 6aGA0+EI4xqAuubLwuyT6X9DgYboN97SvklVpfJ91q2A5S9OUXDpobnw0NUEW5iqEMQ+ R7T90849qp0kGrY9mLqFhgMCLt/2Fx1I+xSSDmbB336S4y/23m0H/8C85BgczDoVdIXY r53Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:subject:to:message-id:date :user-agent:mime-version:content-language: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=rReW1k5GAVJgbNG0UixYUkFg5DmtnjLlfqHFNtL/8e4=; b=BphJzU3EYM+Go+PUhzNZhWvB6CkFdki4QgUHAA13Mfbtxp2LCoGylHqYZ4RROlqLCg +U2U3SoOVxHuAlh6W6ZuHHOOXq/Qfo97EKOPxx6F5neTxLo4Bfiha2inf7yKdlGcsfGT MbiNXg8wNTyn4BbTqey3yAUW3oamMD9J6szPNgRQtGzYUxc2lp2f1+6B71YiQZp+c7xq PXTWeC/w+gU3vJosaC7YH7BYGtkp3NY1k59wsqjXZimx68uPLa7z2vROFSunxAyM5+VJ cNj8TCzmE3jO/306Y1KUCXb8ENOifZLA2WA371dscQDWhJGIz1PY/0oEivEylrMoESvD aRMQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVGUTztUl38kKncjSoccSJkGn0lWMwCSujwEs+b/GPiqTtpbUlt pekyLvu7cVjI1AhTAqnVH48= X-Google-Smtp-Source: APXvYqz0SxrOnw3Gckq2P06IU5kDNXkFQ5iLTUNFWFGBLGIFCq2+gIk9qlX1WvwUt5Zn+ICCwC2ccQ== X-Received: by 2002:a2e:7404:: with SMTP id p4mr14935895ljc.47.1570967831366; Sun, 13 Oct 2019 04:57:11 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a19:f246:: with SMTP id d6ls1059917lfk.9.gmail; Sun, 13 Oct 2019 04:57:10 -0700 (PDT) X-Received: by 2002:ac2:4c2c:: with SMTP id u12mr14291265lfq.104.1570967830565; Sun, 13 Oct 2019 04:57:10 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1570967830; cv=none; d=google.com; s=arc-20160816; b=aLw/cMJb60E2k5e7bkXyPpdR7DVOE4sx0DsSY6g0qAJHjxz1B3oL6L6zQTcFNeOykQ EPqbSPv4+5dj7GPIcgbjoLMBiYctIWKWysMaoBTPWGfsXnFbZIBti4XfiT1TnPmCdNVj z87Wyv/6uJPxdLtYxEPfK+xlw8yoyqKk74JcolOOyCljWJ2IVxmu5wOmxFox6ljFocGu ypA9kb1ot+CW+6i70ZYneQH0GfvQQG8r/gNMBZma9l/4yZJDJx9sELhAYpeTDWR1cpBG gufb+1sl30VJjE4ZGA/UtPmHe44Xv+fHioBRERualZbVEFZ0tMI4T8X7KaPt+rYMygf0 KM8g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:mime-version:user-agent :date:message-id:to:subject:from:dkim-signature; bh=hyD4EKj43xoiNPp3DsD9w8GjjZSXXQh9LvRHB+pRx9c=; b=ih7i3lrQdzcHyurp5ul1gEcgnIgUiNmML0hCx/wAJMPv72HLpRQdUS8ZXo6B21ZyGS bVl6UZBnje8GnwZ9nQEnww8ppRg9p+MQyrbBl3uiD3klrO4YdZCF8jEwg5a7cSdQmG1G mVX339q1X/W5irpi3TToMyiYQfFeFqJY/70U0s2oGbbRxcH/UGWiJgT6WARYBNSq2wuL D4HVkvoDSE268W9yd5wEK+RA0OEz6LwBeVOLZVktOCfP3B6c3Nn4aOi1ex3IpOTepRiP a71qt1prpZj08TcEQY9aWp2N8ZeVkHiNz3BY+JDmO58jdMGYbumubSvRow440K5Y0TNp MnBA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=q8USC7wR; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::334 as permitted sender) smtp.mailfrom=benedikt.ahrens@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x334.google.com (mail-wm1-x334.google.com. [2a00:1450:4864:20::334]) by gmr-mx.google.com with ESMTPS id a9si541018lfk.5.2019.10.13.04.57.10 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 13 Oct 2019 04:57:10 -0700 (PDT) Received-SPF: pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::334 as permitted sender) client-ip=2a00:1450:4864:20::334; Received: by mail-wm1-x334.google.com with SMTP id m18so14092200wmc.1 for ; Sun, 13 Oct 2019 04:57:10 -0700 (PDT) X-Received: by 2002:a1c:b4c1:: with SMTP id d184mr1238159wmf.37.1570967829568; Sun, 13 Oct 2019 04:57:09 -0700 (PDT) Received: from [192.168.1.204] ([31.220.248.111]) by smtp.gmail.com with ESMTPSA id s10sm25612291wmf.48.2019.10.13.04.57.08 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 13 Oct 2019 04:57:09 -0700 (PDT) From: Benedikt Ahrens Subject: [HoTT] PhD position at University of Birmingham, UK To: homotopytypetheory Message-ID: Date: Sun, 13 Oct 2019 12:57:06 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.9.0 MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US X-Original-Sender: benedikt.ahrens@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=q8USC7wR; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::334 as permitted sender) smtp.mailfrom=benedikt.ahrens@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, I would like to invite applications for a fully-funded PhD position in the School of Computer Science at the University of Birmingham, UK. The PhD student will work me on topics related to categorical semantics of programming languages and computer theorem proving. Students broadly interested in these fields of research are strongly encouraged to apply. Topics of particular interest are: * Syntax and semantics of type theory * Formalisation of mathematics in univalent foundations * Directed type theory * Algebraic specification of programming languages Applicants should hold, or be about to obtain, a Masters or Bachelor degree in Computer Science or Mathematics. The PhD position is fully funded, covering tuition fees and a tax-free scholarship. Healthcare is provided for free. Please, do not hesitate to contact me by email for further details: b.ahrens@cs.bham.ac.uk In addition, feel free to browse my webpage for more information on my research interests: https://benediktahrens.net The theory group at Birmingham's School of Computer Science is very active, organising regular seminars and informal meetings. Many relevant international events frequently take place in Birmingham such as YaMCATS category theory seminar, Midlands Graduate School, and Workshops on Univalent Mathematics. For more information see http://www.cs.bham.ac.uk/research/groupings/theory/. Information on how to apply is given on http://www.cs.bham.ac.uk/admissions/postgraduate-research/. However, interested candidates are strongly encouraged to contact me in the first instance. Benedikt Ahrens -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/d5dff735-4e3a-1f3d-6ca4-93dc052ea786%40gmail.com.