From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.2 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: from mail-lj1-x23a.google.com (mail-lj1-x23a.google.com [IPv6:2a00:1450:4864:20::23a]) by inbox.vuxu.org (Postfix) with ESMTP id EC7872539E for ; Fri, 9 Feb 2024 17:09:03 +0100 (CET) Received: by mail-lj1-x23a.google.com with SMTP id 38308e7fff4ca-2d0d451f88csf2688831fa.1 for ; Fri, 09 Feb 2024 08:09:03 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1707494943; cv=pass; d=google.com; s=arc-20160816; b=mxbxlrL2bYuXCsXhnS9RdkVkJaoy7akwWtrYC7LwBRocyo2l8NiEesE7tRpQL7EDfP opwovF+JPWtUKLgfYjxCZCs55OtxoScmmdUbpoeGK4WikQVpLGjIMgWR3GvyMKm+Sols CH2jWeFFGbmRwGbuS2gxGvRi4vRGO8pPOgteQQcCY8gGU2KGoW6OylR1HZh5BskI8mc5 wLKzQiitxB1RZwUIOvUCOye3q0dMQKzG0YQvyP3qSqjImqrbRJ8ISV7hLes9y61AZ/d1 9oG6a0eoF+QWXCijsqsDDVZm+ywBLbbSUUn1bK3rde/FMCpnB0dZKjEX0oEYA0jhCmyn jhEg== 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:reply-to:mime-version:content-language :accept-language:message-id:date:thread-index:thread-topic:subject :to:from:dkim-signature; bh=bFYdC8gzFeXaaoFtONrc7JjZ+ioMIs98tL//HedJirY=; fh=7ur+9uwZyTcb/YOtI3hjtxqnQmzhwdYjiTYUTHrWlGw=; b=p8qMY9WNGPC4ZYnEJlV/pYc1zVi/ewNhiaRylUs1yfduAB9L0vnowPXTRlCQSM0N6/ aLSQQmK39l8PFxfkDkeVXNu7wbK2qGD/GxODjA3o/rQi1U7v6Krg5Ymh+QskKWOQXCuQ UJPX25vpqT7ZDc/KbL7VQ60AKsQQI+O6TBC1WAAQa6Clq2yJJFzS/m7hWkZGElQHcjIF 5MN7RijJ0DdV7c5ZOL6ok/sGaSh2CHe35Bq4HR9k1fTiHeWr0kcfl5naECd7Yy9hxri4 Zi88HJWoZ5etd8HxiHRNNWRvc1hxwZPtXnNYr4eJpCcxs1zT0upE2P85jU0SYuCweFUZ +WTg==; darn=inbox.vuxu.org ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.44.55 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=QUARANTINE sp=NONE dis=NONE) header.from=nottingham.ac.uk DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20230601; t=1707494943; x=1708099743; darn=inbox.vuxu.org; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:reply-to:x-original-authentication-results :x-original-sender:mime-version:content-language:accept-language :message-id:date:thread-index:thread-topic:subject:to:from:from:to :cc:subject:date:message-id:reply-to; bh=bFYdC8gzFeXaaoFtONrc7JjZ+ioMIs98tL//HedJirY=; b=RefsBLLu4DliHJEWcxh4aaW2vpe121/d++d1/eXLwpf/CY868gQGMTc/e3qc44A+u3 6IzayVsXq0NSKGlKpGO462ZN7IsiCoauyMrpLALeea9Q7us0S03OEpU+EdLhBbmMwq1i FrYdWBOTY1tgFT7Aecwl8dFHyAJlY4hCOGZ6b8W6ZrV0gjqk1Gxw7I2pvt1gwB2T1iPK lfEerIdHhMjpbRK20lRsL8hJAkaquMGTX00io2bmE4XHC1ovsqjZZSLykXGIIrnAhWwX D3D93RZQIH2nqWrFw5uQOYSNL7NmwU184ltP4u6NPlsqQvabIlP3v9GPdQ4QGMGg1nZi vYVw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1707494943; x=1708099743; h=list-unsubscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence:reply-to :x-original-authentication-results:x-original-sender:mime-version :content-language:accept-language:message-id:date:thread-index :thread-topic:subject:to:from:x-beenthere:x-gm-message-state:from:to :cc:subject:date:message-id:reply-to; bh=bFYdC8gzFeXaaoFtONrc7JjZ+ioMIs98tL//HedJirY=; b=Yl4C3N0HkafEhHLAsgsXryOFq1z8FdwwOhKkc9I8BHQ5H33Tp1Q7TMA9P1WT7QL8Vl pw9ECj7UA9WSucBKx35HhJHRoprzKU3iloNXzUawdkC1kinYJId7QVcAlhsW8mXBuYD7 rAIHBUq8A9f1DmiWjLVxMe3LSELvmVCRdDwem+dhn1RcN8fcfsRaNXSog0sR7InkxxrB vyHznyRrHZDJfV3afaRPcxmJBnNqzD2q/kTlgSWlBP2yZ63JHJ5RB9tj4lDK9DcDeeju HC4hkOH/tGgSakxY7nAyC5wDnXhkaPegxIHAJa1yCzzoAFJoieFlhn6KniOgrGHNvWo/ 0DNw== X-Forwarded-Encrypted: i=2; AJvYcCWOpp6gabYGytRlT6dTYnWAjIqAsBL8NVAdOOuL35hlYGqRTdhadbznLQ4c5MYHBVtgk+9pJ2jKUkhm3MMnlnuyqw== X-Gm-Message-State: AOJu0YyP+jJ5z9oBuRmqJJohbxCO2hwdnHMO5NZR724QwHui3eWo0tGm I8u01Y8amEjoHkdLbH3uQopHo79PD+fKdtsHkHWNNmp1um0um220 X-Google-Smtp-Source: AGHT+IHA7VM6DVarCjTSW4Es3UUAcQ3edSHwAUGH3nM1eJItcrV/A//gS2kUmI55xr3+iMp3PFoC0g== X-Received: by 2002:a05:6512:3c86:b0:511:4881:1b7a with SMTP id h6-20020a0565123c8600b0051148811b7amr1745742lfv.4.1707494942484; Fri, 09 Feb 2024 08:09:02 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:34cc:b0:410:5daf:3d27 with SMTP id d12-20020a05600c34cc00b004105daf3d27ls468764wmq.0.-pod-prod-06-eu; Fri, 09 Feb 2024 08:08:59 -0800 (PST) X-Forwarded-Encrypted: i=2; AJvYcCU97C4XiiWVJrZy9tr1Z9l1jLMX5m1pgO56uA9lmBJE6nJGKvTKY7G1fu0ZsqJC3xVEEs+89lD/gqZty1z+jihzR0yjcR0wV8YsuDt8wKoVBfbYEw== X-Received: by 2002:a05:600c:45c7:b0:410:6d13:79df with SMTP id s7-20020a05600c45c700b004106d1379dfmr1433639wmo.10.1707494939172; Fri, 09 Feb 2024 08:08:59 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1707494939; cv=none; d=google.com; s=arc-20160816; b=wH/KV7RPOa/TfgNqNqEh+KXmJPMtNepEwqfp7iYEJwYTbe5ETIfDHlkyc3utfBiV7/ n0++ZyLAbzUnNzg4iNas354bBwoUjW9uK8cKWrqJLw0fadrxpDgAiT51IobrO1Qc4MrZ gj8EtbcdFUmYhBz/IJ9X62VBHfD/kUyxrXOgwm7qVpFs0KH+lQQE9DIxhwJi+xDTx9m7 p5iaBQdljM/NzliCrWyAolZDH7r7iRG18BJhVl8Gpnw4Z/51oXpHqxlzi7CY3FCQm69z BXPPMyxLo39lAwfMHxVQkElPpcFQEFvTv/voMXTB6RxKItmJVoHBtTL0r8j6luc5vseB obTQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-language:accept-language:message-id:date :thread-index:thread-topic:subject:to:from; bh=mJt9ywNnhzt6FIL6tqkuzLVJMN3o/dAbBbPpW2FJFFY=; fh=nu3VgzZni6MQCYEdxv6iuxSlaL6KIokIp09aWjqLfIM=; b=m9ZUbryDj4YLyJU0UzPPpZgcCWq1dLV8oKekJO7QJy8nYaDyy0gZZNoLa5HPeSC58N RrJSc01PAGAR+knN3WYIrD8NqvMEYq7unrZeVJrSlNqVb+92SIiTJ5qR/dsuuO4IYa/b Tg+9sbI7vCJUSkMaMU6DzMYhOqhs8FElrjLnp3vlFZSqHrj4kRj/HLJ0js+HOCtC7Cyc XT3x2b9U5PXcct9t6tSAidVlZJdiZBX7USvNICE9OX5ZaruDQULTgzis9Ogkumla5fKO Cwz3uVCJbJQnK0YgILsjVqhEpgc+gx6aFQQ45z1zWxx4Wkmdqt8d/YkiK43Sz6k2E1Ae xXxw==; dara=google.com ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.44.55 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=QUARANTINE sp=NONE dis=NONE) header.from=nottingham.ac.uk X-Forwarded-Encrypted: i=1; AJvYcCX+095DOOifXDHnRwoBU7X8Wlplxbhqoest9a79sFa0dkwPedyA8sa2A5vgiC3MXpvL3i6vfjNAthBVR2qbiEuE6Lo1K30P3uaxtBWXKPgx44vnwg== Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk. [128.243.44.55]) by gmr-mx.google.com with ESMTPS id p37-20020a05600c1da500b0040fdf202988si53729wms.1.2024.02.09.08.08.59 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Fri, 09 Feb 2024 08:08:59 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.44.55 as permitted sender) client-ip=128.243.44.55; Received: from uiwexedg02.ad.nottingham.ac.uk ([10.159.172.14]:28246) by smtp3.nottingham.ac.uk with esmtps (TLS1.2) tls TLS_RSA_WITH_AES_128_CBC_SHA256 (Exim 4.94.2) (envelope-from ) id 1rYTQv-0000CJ-KB; Fri, 09 Feb 2024 16:08:57 +0000 Received: from UiWexCHM04.ad.nottingham.ac.uk (10.159.186.8) by exchangeSMTP.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.2507.35; Fri, 9 Feb 2024 16:08:57 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by UiWexCHM04.ad.nottingham.ac.uk (10.159.186.8) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.2.1258.28; Fri, 9 Feb 2024 16:08:57 +0000 Received: from UiWexEDG02.ad.nottingham.ac.uk (10.159.172.14) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.2507.35 via Frontend Transport; Fri, 9 Feb 2024 16:08:57 +0000 Received: from EUR01-HE1-obe.outbound.protection.outlook.com (128.243.226.54) by exchangeSMTP.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.2507.35; Fri, 9 Feb 2024 16:08:56 +0000 Received: from PAXPR06MB7869.eurprd06.prod.outlook.com (2603:10a6:102:1a0::20) by AM9PR06MB8034.eurprd06.prod.outlook.com (2603:10a6:20b:3a5::11) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.7270.24; Fri, 9 Feb 2024 16:08:55 +0000 Received: from PAXPR06MB7869.eurprd06.prod.outlook.com ([fe80::cdb1:108e:21e0:ab1c]) by PAXPR06MB7869.eurprd06.prod.outlook.com ([fe80::cdb1:108e:21e0:ab1c%6]) with mapi id 15.20.7270.025; Fri, 9 Feb 2024 16:08:55 +0000 From: "'Thorsten Altenkirch' via Homotopy Type Theory" To: "agda@lists.chalmers.se" , "coq-club@inria.fr" , Types-announce , homotopy Type Theory Subject: [HoTT] PhD positions at Nottingham Thread-Topic: PhD positions at Nottingham Thread-Index: AQHaW3Azu9Ph8zz6pEWmbnew/8DHfg== Date: Fri, 9 Feb 2024 16:08:55 +0000 Message-ID: Accept-Language: en-GB, en-US Content-Language: en-GB x-ms-exchange-senderadcheck: 1 x-ms-exchange-antispam-relay: 0 x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?us-ascii?Q?LeOEbs+TPOdo5PI7dqhL2qhSx4n/DEszy0ED2ENFJUMWPFAVuEJS8TFRydHz?= =?us-ascii?Q?aDxsOPzoOHNhOReg1tbpQ4Ne1GG9Q+q0oGnY15ufVQiMQTpLjvjGijAZjaGq?= =?us-ascii?Q?4RCWVdSFyaSDkHO8BaH0Kyyrko+cLxY7RR3+chfU+7rRr74FGJp8IlIRThI7?= =?us-ascii?Q?yhYOm2HM1PxPZhxwX7BCkGGoK5AgpVeE/WpyYu0wX6s2RfoAi0miEssCT0Cp?= =?us-ascii?Q?g1obMPNZKja5H44XnFQFhOn7NUR3kjv9eeUKBUDQptRgLQOo8os3ErG4ycnm?= =?us-ascii?Q?CneSXZNcrKbH89z0d9m0f7mEwmtnjvv8GYytNhkw/+VbGhPoyv5SerKJd6if?= =?us-ascii?Q?LKgdQl++CZFB0kggmnV4VQoMloJNHBssI8+b1hOhJGdZJCd5t65ZAl3Hgd9q?= =?us-ascii?Q?/E9XePz5sPaS59om2lgCGN6G8/6Oxj984Xzi8K9iay9h/gI9lRISwSYtU7Dk?= =?us-ascii?Q?paT+elF4DZoeq48jScKLemUQm/TYFkYyKSByt3sBus/RZy1iLjjlaVNBmJDK?= =?us-ascii?Q?5JwclYyO5RH1JKcGhY/NoTcr02OkKadhW8n3AiHrg0Ym/zud1I72pMoqYp5W?= =?us-ascii?Q?cAHfFTbTsvPVt9t89ND506KoZow0X60tR93d6COaQ+nxBKL99TYEZgRUpBun?= =?us-ascii?Q?mxfTaw+BT2xmqoZbWZxuU+4U1PNJmRiVV7Wk157dPJ9xn1+LIlRCpdld6vDF?= =?us-ascii?Q?FmNEsYCa61EKn8aQFhQSxCI6Av81ZRD6zDvK9QbZRuN1JJmofgQ/Qoyezyr/?= =?us-ascii?Q?3CR1lufSEantF0ErPJdLHVBE3Qo+hMxX8KLMMi6n98MQD18+pbRY/1/1sffC?= =?us-ascii?Q?37X5+OvTAT57OzASEdg/mtUDYgSFdIuXqZelNEy3tdC1g9qJqnzz5oFuag49?= =?us-ascii?Q?zqNlNp7kqt2zI0Rr95C8w5cHlT4VUWQrgx/0UGW1lOjwgrqynhiHhgVWZSvi?= =?us-ascii?Q?qtk/kYyRQyTxXnD9CdazMhAMU5wvcPRAqR08Bx3v3zyFbAUEnhCtovdKeAS3?= =?us-ascii?Q?WWtFZ9buyy24cyQZTzRtHELKk5mXDks7Plq8vACRt9qLjZ55sUIWEOayk4ml?= =?us-ascii?Q?IXOnsNgBcZtX4cfI0CJINO9+iD8UlCqtMiOdixzRqmmEzfnUsIKy3LsR/DA5?= =?us-ascii?Q?hVJpsNpHA4ZO5xezmW0uC/+nWYXZB0YgK474WJdC3itx3Hsj/64Tfr162iKH?= =?us-ascii?Q?y1bcSGwAMbb3wod5tjrhgr4hfhl20JQ9MqYo64+uL+DFO4OW3PAMkQilcnib?= =?us-ascii?Q?O7nnzQ5L0SVmE1M1/nYCXP+qa8M5MMlethK1vh8vJqisN9Ip6/bm6MwW+Qzb?= =?us-ascii?Q?mzGBzGZNl5zEgGtA4vtTGju9GCka8oMtskBqLOMkddR0zzu/Bk4n4j12YKTo?= =?us-ascii?Q?ZgejMxlHnYqWSpZbI4nEWtBV09/KyoBTabgiEEHd6CICuA7bJdMiXP6aU9Zi?= =?us-ascii?Q?qCok1h+FSQDaUGUvu9G/zFsPhAYjoJZz8UtIEVg+2dU+qOkidPWGuIKxBVVS?= =?us-ascii?Q?/XzomRv0eMyilRtoDNy9F/eg3rIIwkfB06xuYNov4A/ominQk9bYOecW7B3t?= =?us-ascii?Q?K/QUUMHIf7MPmXaXVVls5o9eREA4MvptSs+M5yTAJrhzOYBoJv+AcCqDKDvu?= =?us-ascii?Q?T83m1JHBHIrk+sI3RD8QChT5ZpydUMudONTBEnoLy/G2?= Content-Type: multipart/alternative; boundary="_000_PAXPR06MB786905044BBBCC4FC0F71EEDCD4B2PAXPR06MB7869eurp_" MIME-Version: 1.0 X-Original-Sender: thorsten.altenkirch@nottingham.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.44.55 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=QUARANTINE sp=NONE dis=NONE) header.from=nottingham.ac.uk X-Original-From: Thorsten Altenkirch Reply-To: Thorsten Altenkirch 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: , --_000_PAXPR06MB786905044BBBCC4FC0F71EEDCD4B2PAXPR06MB7869eurp_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable We are advertising several PhD positions at Nottingham which includes the Functional Programm= ing Laboratory. The group which includes Nicolai Kraus and Ulrik Buchholtz has got a strong= interest in Type Theory in particular Homotopy Type Theory and its semanti= c foundations using (higher) category theory. We mainly use the agda system= for formal developments. If you are interested, please contact me before applying. Cheers, Thorsten This message and any attachment are intended solely for the addressee and m= ay contain confidential information. If you have received this message in e= rror, please contact the sender and delete the email and attachment. Any vi= ews or opinions expressed by the author of this email do not necessarily re= flect the views of the University of Nottingham. Email communications with = the University of Nottingham may be monitored where permitted by law. --=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/PAXPR06MB786905044BBBCC4FC0F71EEDCD4B2%40PAXPR06MB7869.e= urprd06.prod.outlook.com. --_000_PAXPR06MB786905044BBBCC4FC0F71EEDCD4B2PAXPR06MB7869eurp_ Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

We are advertising = several PhD positions at Nottingham which includes the Functional Programming L= aboratory.

 

The group which inc= ludes Nicolai Kraus and Ulrik Buchholtz has got a strong interest in Type T= heory in particular Homotopy Type Theory and its semantic foundations using= (higher) category theory. We mainly use the agda system for formal developments.

 

If you are interest= ed, please contact me before applying.

 

Cheers,<= /span>

Thorsten

This message and any attachment are intended solely for the addressee and m= ay contain confidential information. If you have received this message in e= rror, please contact the sender and delete the email and attachment. Any vi= ews or opinions expressed by the author of this email do not necessarily reflect the views of the Universit= y of Nottingham. Email communications with the University of Nottingham may= be monitored where permitted by law.

--
You received this message because you are subscribed to the Google Groups &= quot;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/PAXPR06MB786905044BBB= CC4FC0F71EEDCD4B2%40PAXPR06MB7869.eurprd06.prod.outlook.com.
--_000_PAXPR06MB786905044BBBCC4FC0F71EEDCD4B2PAXPR06MB7869eurp_--