From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,HTML_MESSAGE,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 12705 invoked from network); 20 Jan 2021 18:38:30 -0000 Received: from mail-lj1-x23f.google.com (2a00:1450:4864:20::23f) by inbox.vuxu.org with ESMTPUTF8; 20 Jan 2021 18:38:30 -0000 Received: by mail-lj1-x23f.google.com with SMTP id c8sf7077086ljj.3 for ; Wed, 20 Jan 2021 10:38:30 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1611167907; cv=pass; d=google.com; s=arc-20160816; b=AhGf62xECv3bx0u67mJCXv6C5GjTSHQejCYDHOJO5eVlTGOheuoxv77cbjCA8JWtr3 ryrq0N+u91DlxoD+4ZiOLXOnrMuBuNSl8KTcJz4mTNgPDobL2RuYFjUJoszt5KCFLWI4 fpRLvh7kKqI/EBQn5hRIc8KQYaef5NQfrn4kmUQ7QqDUyRJvyeqkEVxfVyM9c1VXaMbr MTaJm5CYREcUtgImiKCdkIIb+L/l1q4jDuzUSL+JdG7AebKz0mRpAHAfcNod8lwMvvpL lUa18eAGbvXjcAz7tZjumVfRJ69Bdhz78+3OoNiON0VwFlkKnOUg51alaDEC7M7BSbmy t+ZQ== 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:mime-version:content-language :accept-language:message-id:date:thread-index:thread-topic:subject :to:from:sender:dkim-signature; bh=b8VUsyIFwgpGIcXbHqDlvZ7PKamtlPCt6NcVbLzP/ro=; b=De41INApn4NBc9zPl2lJEbhzAlujNJ4iA2d/SbAsRk9CU6LMsa3ymmG3fpIs992GHp Qd93t/6PlBl8hd4Gm+ShsKNjCRYtc6C1tPcfpDZlei6TnHaI+zdQG/pPDQjMAhTZ1cqu wqrarJF3bcig3HkqHa7uG/cqFESNKnP0VwGhh5dpR+bWegu1w41n4HYk58+xpWqqqO8b wG1PVJKF55wL3Ba/GE58xFtwAkHW8tUTinjmzDl0gJz/qUhQIfmLlsn8DA+j13CjiFQM /+Gy76Zcmbhk3goF8nXZtMSI6QiSuBLrliwP7M6nBVBBmxKTxT2j9iRddWoq3+WFiPab KJjQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thierry.coquand@cse.gu.se designates 129.16.226.132 as permitted sender) smtp.mailfrom=Thierry.Coquand@cse.gu.se DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:subject:thread-topic:thread-index:date:message-id :accept-language:content-language:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=b8VUsyIFwgpGIcXbHqDlvZ7PKamtlPCt6NcVbLzP/ro=; b=h51vc77ejfROjOGq5CuqYXZSPvAoSwsGLzv57x2VEF4+80w1piOLVOP1ODGUnQ4Uoo i82ifaLjqIJXU81amBBX/qMvdYHlpa0pEntupaeKmj1MAj8WVXhC+YOO/+3Bz5y0o0L+ AJCMBdGtr7aHUQTU961VrtiGpFxHU6NllFNOuzrB+GR1R0kjPex9Cbvp6QuUmh9LxGpK yv/hXLRUiGf3oF+WcyAA22V1R56egUSx6ZQRQJy8/sosDolD2gQZSCyaJHBNoAJBGioX mUhjYUai9n6Gfw4HrG76bhQ3ZDvdc7v1jmhkRjGR3akYUxyyW2KvTP9louQ6lHTVzEDn DvRg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:subject:thread-topic:thread-index :date:message-id:accept-language:content-language:mime-version :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=b8VUsyIFwgpGIcXbHqDlvZ7PKamtlPCt6NcVbLzP/ro=; b=QFa7gmEPcC5XE2BDTuvWjMtRuMvlEFJWZmO4/4DSq1opBah44DcmUz4jvJEUssAz+0 4GvXDmsaIA2LzFBJAhDRcwldm1m7Chnoq58mroy/LMt8/UVAPYTNQ3bOdYRV4Pfc0Jn/ bRWO4cbhNRC9+97wNXzvj+vagp8o1XcEVR8/p4EYIYQmcefINl6sjGBGNExHoXGVsGkD Ar5JB0WKM9IAUbTM3lhQM8lXqjBEvS1yKwRFAGPYDgSgxkkuAmpUV/1xSXt31qd4Z9UM 0rQtQHZjRXMDiTIaBrdxBH5J/fN4YWVjwwSN+99jduvBAafVssZbomCa/FYTME1q6cN4 wu+g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532+U377SG75fjQz+wCus43IFF01w25pCXsNZQfpPS+I4Ai7bYQm F+MljIpbDOisgqOmQcK7Jms= X-Google-Smtp-Source: ABdhPJzktLAPXeM75ECfU6A7qSEgZZvXv4ZeMD3nMRyztwnyCvxtPc/i5Cm84PzGAY5SrzCAXO3LuA== X-Received: by 2002:a05:6512:202b:: with SMTP id s11mr593605lfs.285.1611167907404; Wed, 20 Jan 2021 10:38:27 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:3001:: with SMTP id w1ls4311753ljw.3.gmail; Wed, 20 Jan 2021 10:38:26 -0800 (PST) X-Received: by 2002:a2e:8eda:: with SMTP id e26mr5052872ljl.272.1611167906307; Wed, 20 Jan 2021 10:38:26 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1611167906; cv=none; d=google.com; s=arc-20160816; b=ZYJwVJUclinPRw3GZMiVcmXY+Ee73Wh9GDAvyxgbthIMArl85ed/RYtleFwTvqCJ/w A1eSW/FsYKeJ+plfef7s0za9ZtxS2KMORTQm1s7JLhogJByOBZ6rduA/jE8qWhb7q3OW 7rcGy3JBw0jOn22yUO5Fag81md4O7VVcHwoLpQsoWb/ZoSH0Rn+YzRvVKqecZGu6N5vR IRqJADKP4zu5JP1iTS0/jB7tDhufN3y5VN7cSWmWR/ApuxVh+IZh4w4qX9WCJy3vX/Pv /jSjVBvg3JcbSWYG1kpxhTuHCOvio2gtWL5eryQMh5MS6nxW/CsQR80rB5QAR2LWaV+8 voTQ== 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=+RxMVm0LiFuQ04AVBUXswNrjp9WODaE8twCWrb8iiis=; b=bDfr893a5kKVkQZwPefGt1N79w0M4DfAPBIG+p4En9tAROWOfienkEACWJElP9G8Hn nvuLjxzJOiO+nXeBgFeq+2ZRYcDq1vXoAZfNz4A4WYDHp3+S/2LcMEROClF9VgFCk81e iUu2kb72jFrf4u5ypFsscX19xq+iOYUlGd1Sh9qNF3LxXwyyicZNDBtShZaZfzfmiTyX FiGkZi/yrqcFhImJcCdRvPIkMCm0DFvxdHyTXOcmg2+sOamu9R+5U0nvubjwJUCqRFyz EMiOXYk39DxZ4IHcz1e5wV36vEXvJWnUiPhRg2d5b0KPjOg6uyCJbDom+PXe5sq25jXU P+tA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thierry.coquand@cse.gu.se designates 129.16.226.132 as permitted sender) smtp.mailfrom=Thierry.Coquand@cse.gu.se Received: from tyrell.ita.chalmers.se (tyrell.ita.chalmers.se. [129.16.226.132]) by gmr-mx.google.com with ESMTPS id z4si200250lfr.7.2021.01.20.10.38.26 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Wed, 20 Jan 2021 10:38:26 -0800 (PST) Received-SPF: pass (google.com: domain of thierry.coquand@cse.gu.se designates 129.16.226.132 as permitted sender) client-ip=129.16.226.132; Received: from tyrell.ita.chalmers.se (129.16.226.132) by tyrell.ita.chalmers.se (129.16.226.132) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.1.2176.2; Wed, 20 Jan 2021 19:38:25 +0100 Received: from tyrell.ita.chalmers.se ([129.16.226.132]) by tyrell.ita.chalmers.se ([129.16.226.132]) with mapi id 15.01.2176.002; Wed, 20 Jan 2021 19:38:25 +0100 From: Thierry Coquand To: "proglog@lists.chalmers.se" , agda mailing list , "types-announce@lists.seas.upenn.edu" , "eutypes@cs.ru.nl" , Homotopy Type Theory Subject: [HoTT] two fully funded PhD positions in type theory Thread-Topic: two fully funded PhD positions in type theory Thread-Index: AQHW71tww92gY14RrkuliX79eAcuYQ== Date: Wed, 20 Jan 2021 18:38:25 +0000 Message-ID: <1B889378-403D-412F-AEAF-A91C62348D18@chalmers.se> Accept-Language: en-US, sv-SE Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [129.16.10.245] Content-Type: multipart/alternative; boundary="_000_1B889378403D412FAEAFA91C62348D18chalmersse_" MIME-Version: 1.0 X-Original-Sender: thierry.coquand@cse.gu.se X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thierry.coquand@cse.gu.se designates 129.16.226.132 as permitted sender) smtp.mailfrom=Thierry.Coquand@cse.gu.se 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_1B889378403D412FAEAFA91C62348D18chalmersse_ Content-Type: text/plain; charset="UTF-8" Please distribute to undergraduate and master's students and appropriate counsellors and supervisors. We have two fully funded PhD positions for work in type theory at Chalmers/Univ. of Gothenburg. Observe that you will get employed at the Univ. of Gothenburg with full employment benefits (health care, pension, etc). Our research ranges from foundational studies (models, homotopy type theory) to actual implementations of interactive proof systems (Agda). The research group consists, beside myself, of Andreas Abel, Nils Anders Danielsson, Peter Dybjer, Ulf Norell and Christian Sattler. PhD positions usually extend to 5 years, where every year you spend 80% of your time reading courses and working on your research, and 20% on teaching. Deadline for application: February 14th 2021 For information on how to apply and whom to contact if you have further questions please visit this link https://web103.reachmee.com/ext/I005/1035/job?site=7&lang=UK&validator=9b89bead79bb7258ad55c8d75228e5b7&job_id=18601 Best regards, Thierry Coquand -- 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/1B889378-403D-412F-AEAF-A91C62348D18%40chalmers.se. --_000_1B889378403D412FAEAFA91C62348D18chalmersse_ Content-Type: text/html; charset="UTF-8" Content-ID: <34C13E2093B7CE4488D1A33CB885670D@chalmers.se> Content-Transfer-Encoding: quoted-printable  Please distribute to undergraduate and master's students and appropri= ate counsellors and supervisors.

We have two fully funded PhD positions for work in type theory at Chalmers/= Univ. of Gothenburg.
Observe that you will get employed at the Univ. of Gothenburg with full emp= loyment benefits (health care, pension, etc).

Our research ranges from foundational studies (models, homotopy type theory= ) to actual implementations of interactive proof systems (Agda).
The research group consists, beside myself, of Andreas Abel, Nils Anders Da= nielsson, Peter Dybjer, Ulf Norell and Christian Sattler.

PhD positions usually extend to 5 years, where every year you spend 80% of = your time reading courses and working on your research, and 20% on teaching= .
Deadline for application: February 14th = 2021

For information on how to apply and whom to contact if you have further que= stions please visit this link

https://web103.reachmee.com/ext/I005/1035/job?site=3D7&lang= =3DUK&validator=3D9b89bead79bb7258ad55c8d75228e5b7&job_id=3D18601

 Best regards,
 Thierry Coquand

--
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/m= sgid/HomotopyTypeTheory/1B889378-403D-412F-AEAF-A91C62348D18%40chalmers.se<= /a>.
--_000_1B889378403D412FAEAFA91C62348D18chalmersse_--