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=0.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,HTML_OBFUSCATE_10_20, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 9392 invoked from network); 17 Oct 2022 22:11:04 -0000 Received: from mail-yb1-xb3e.google.com (2607:f8b0:4864:20::b3e) by inbox.vuxu.org with ESMTPUTF8; 17 Oct 2022 22:11:04 -0000 Received: by mail-yb1-xb3e.google.com with SMTP id o4-20020a258d84000000b006bcfc1aafbdsf11628863ybl.14 for ; Mon, 17 Oct 2022 15:11:03 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1666044663; cv=pass; d=google.com; s=arc-20160816; b=dnLDsxQ0YLc98HAdIjf1lV3Yr0Fv9CccAJ5fTAm91FI4vY+xcJgksX3StAZFtoUhN7 wI1uJbztP00QjMPgQJ0U7IqXJYqHZkwq3VeF+q+f0RRVLQGEij4IvjLFhTJEvhG5njb2 OoUKGNV3gQ9Rn73qtN/DnrO0jOnfiFPgZWgLThGJOoZReKpG0twXtpw0ehb1MFmQUTdU eXlatcsmPtlvIWOwtPuXVNJRuYS4KZV7WJTWwCxkbfLxdizInbAhuWdvLXBS/oGd364v pIIaJbmdf5lDN3FHfGdAvcUOKrl4dQBlPmo+g96MhSj6KChwK10kkr2BrgNrTBCFw/8X 6h4Q== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=ieO5RV4UYqrYq2lLUDvMeFdzgykM+I1dg3K8zgxIRNo=; b=prM+IiKqI8R7xSSOYDRuCVZid5shppWlXJHJ35lGhO7RRVgy57yTBYMgiSF4gzlpLt fkOp6wtf05DZwBh0dWM5nkHKDMDrAe3PX3RJGwgL6i2EFuB3qbzLT2v2tnsuM3FLac6N dRGvnjBhvnef0mK+VvwfCh6IUw/EW3FMvrdBRg8dPMO3WOCHmYtnZBVDvyiU5TMl7EKt pv+BtWS/DRu+6fgVxVmX/n+KgtMmQL3oR1twuqZCs1WzpETHvr1q+GYZ/kU8uAddkAQ9 /kYspnlANen9gjMGbQaHxglH0ayt7TPZToXSly0ulfBCzHwLP0ekpWnuLeJbAxlpJMAn b/3g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b="TEO/4ohW"; spf=pass (google.com: domain of sattler.christian@gmail.com designates 2607:f8b0:4864:20::102d as permitted sender) smtp.mailfrom=sattler.christian@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=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:to:subject:message-id:date:from:mime-version :sender:from:to:cc:subject:date:message-id:reply-to; bh=ieO5RV4UYqrYq2lLUDvMeFdzgykM+I1dg3K8zgxIRNo=; b=ZDUCn8EuNGdMhqf+mUOFSw9gna2xSSAu1CWeDPinu1cB4WLPomlAvH3TB+g2srC/Jf aDGYuH6hao2fCy6qpumpK/RQi01rEbkggAIOr/9WpvP/I9Qxd/JnvgeJo710WJvW/eIn qs7PSyOa+w0Atrt7XRTSRdbzJBBF0t0dS+ZlGk64Vkbt3sofTjCZ+POSJff7m1Fr0Bpk /Oor2CjFbfXrht/aNpPLOsIP8f98eG2BCKn0FJOOQCkrponJ0zXqP1RBQJiZACVjwjjG uCszzrwUS/LimLVBSD7ydRTKZXSR0y2QpaWv/R7M6pQDUzRVbuRdXivG8/VLxwUf4+ZC TlRA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:to:subject:message-id:date:from:mime-version:from :to:cc:subject:date:message-id:reply-to; bh=ieO5RV4UYqrYq2lLUDvMeFdzgykM+I1dg3K8zgxIRNo=; b=fgI3vB0cxyecLwB6P810GW3ewZESg4GWseFCQj26PA074cVq01rTyQ7XbwDSpH0C1m uJPdYN9fxHnIL/cDItkTUzfRANrcREhqXvDTv4mh2mQ+TJrQA1cBEx0do5qwLU4bcnQ4 hiFPx0ZbzB7EFLRlLtmwgw81vAz9D8CPR+ympGFAOqzrkbxOUbCAfQjK0paBpXEQaCNr sNMTQ94KXNVky20hsz4bJ0JgMyRWyldfjzuEpqzs2OIJD24ciF5MZExa8DMxDMRgwAFi 1zA8p6u9a1rQfaBNGTYFDYlnaGUFwLP130fHAj7zE1sOqktUwGeWkpF7UPg1+GzFA63a 05/g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:to:subject :message-id:date:from:mime-version:x-gm-message-state:sender:from:to :cc:subject:date:message-id:reply-to; bh=ieO5RV4UYqrYq2lLUDvMeFdzgykM+I1dg3K8zgxIRNo=; b=G3O+q5oIWLYXwudv+HVANUqxNavG7SnJglkndEu2TiQz0FYkQlEIXNmK5h/wgw9VM6 +DD19yGNi1eec4Kh+dCs3gE6tiQqM8GEF9UaEQAnu/2pw1yV2ch9EtYMqzNX8yRAyKvn SudKePzrp+yR4WY6UsK7lICLmbDGO8X1Xgr9UlKV4GhJYbyJ5YnyWr4q1YLk+IUeXUty qy7ap540EouEavM3ImUlBVjx8XO1YcudZ2GSuVi0mfHQ7GpVKDpXUPb0grrJeoix5IvP VVWMWJFP8sEt9o4cZrxQBzZZhEz9TeaHUBWsc38Vc+kbF/SjUczuC5rd5Zzz0bxuDASy 51dw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ACrzQf00rM3PVnkw0VXcDmS347TbwQcfNJEEtK4Ua+u3lb9xr1BtzYiU qb5kbUrCojoiFl/BP9q7uoY= X-Google-Smtp-Source: AMsMyM5Q1EmHxOaekNNJxUP2a6NdUhn960Ja3gOObDlUoYzChnmfnBuy0kuMlcpzT9QkO1II9PjbRA== X-Received: by 2002:a81:1a94:0:b0:360:bbf0:f50f with SMTP id a142-20020a811a94000000b00360bbf0f50fmr10925386ywa.239.1666044662465; Mon, 17 Oct 2022 15:11:02 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:c213:0:b0:34d:180c:9d3b with SMTP id z19-20020a81c213000000b0034d180c9d3bls4971386ywc.3.-pod-prod-gmail; Mon, 17 Oct 2022 15:11:01 -0700 (PDT) X-Received: by 2002:a0d:c685:0:b0:361:1fb9:e8fc with SMTP id i127-20020a0dc685000000b003611fb9e8fcmr11235046ywd.508.1666044661055; Mon, 17 Oct 2022 15:11:01 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1666044661; cv=none; d=google.com; s=arc-20160816; b=miinK9DMmvyesJKhDAbhh+XNCB0wtGkNVD2SP5gmSQYZqxmTOnE3ZYgp6L3uogAxXZ LnWFVnX59RXooLUi5sJtrA3rmLDc0TqT9wfhpQxbfoWElv7WQsZAMhu4eXKds4+IWOOr 1oaLAXuGLWpMRazgRmxqL7pvCNyyQVhm8qhFQyUTpJlj2KykMuqvAZFVaGm9xBX4swxQ M9IKNVxmxsWlxxVKPzgGrYliOxxPp8m4TOYWSU8ETfsoRQe5TQN8/HM2BoKnJjL0yytc IiU2gYzX9nm0n1Su/if3vUVLpegFmh3LXaklAUrABENOK/2F6xKzDhLtkgBwDEcepTUm 4yJQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=uR59cChSDZZMUvXF4cQ86J+XfHfy+an3LWezMCvzfgI=; b=X/j+CQGQf8dzdWKkMUaPkj1ABZRevWtdY1xXYFpnyOGGV8xNfFtIvbs+6ff2iBby9o fyQtfW60c1lIOMMvJhKlg4x8c/lBJeXYLeE6W1bgBko+QMgnllryvEH/xPKzeu8QuiBt uwCtCc3IF1UfeyKwlrHaj7yYMv3aRbRv+0mLlkpH0gPUqZLPNapabKlCHkz2WHOe1/vJ k7WM3BJi3wplRqiUEnXeEmSGzVlwtzJOlniWlERQs5mjFh5RXOIwdq98fKoAjt/FsKyR 0SIAnXpgdj2PnUt7mz2ndq1GQJ0WcgOJOk0hy9/K7VrGR8iTVVlmCWjfyxIjoLrU0j9d s1Vg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b="TEO/4ohW"; spf=pass (google.com: domain of sattler.christian@gmail.com designates 2607:f8b0:4864:20::102d as permitted sender) smtp.mailfrom=sattler.christian@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-pj1-x102d.google.com (mail-pj1-x102d.google.com. [2607:f8b0:4864:20::102d]) by gmr-mx.google.com with ESMTPS id f5-20020a25bd85000000b006c40eb212dfsi122134ybh.3.2022.10.17.15.11.01 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 17 Oct 2022 15:11:01 -0700 (PDT) Received-SPF: pass (google.com: domain of sattler.christian@gmail.com designates 2607:f8b0:4864:20::102d as permitted sender) client-ip=2607:f8b0:4864:20::102d; Received: by mail-pj1-x102d.google.com with SMTP id 70so12213041pjo.4 for ; Mon, 17 Oct 2022 15:11:01 -0700 (PDT) X-Received: by 2002:a17:902:9b82:b0:183:fffb:1bfe with SMTP id y2-20020a1709029b8200b00183fffb1bfemr14098069plp.173.1666044660361; Mon, 17 Oct 2022 15:11:00 -0700 (PDT) MIME-Version: 1.0 From: Christian Sattler Date: Tue, 18 Oct 2022 00:10:48 +0200 Message-ID: Subject: [HoTT] Four PhD student positions in Gothenburg To: homotopytypetheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000292f5d05eb42406e" X-Original-Sender: sattler.christian@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b="TEO/4ohW"; spf=pass (google.com: domain of sattler.christian@gmail.com designates 2607:f8b0:4864:20::102d as permitted sender) smtp.mailfrom=sattler.christian@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: , List-Unsubscribe: , --000000000000292f5d05eb42406e Content-Type: text/plain; charset="UTF-8" The logic and types group at Chalmers and Gothenburg university is now recruiting *four PhD students* to work on dependent type theory for mathematics and computer science together with Prof. Thierry Coquand and others in the group. The project is about homotopy type theory and univalent foundations, where type theory is extended with univalence and higher inductive types. The selected PhD students would be working on topics ranging from theoretical studies of models and connections to higher category theory to actual formalisations of mathematics, but they could also work more oriented toward implementation of proof systems, in particular connected to Agda. It is worth noting that the selected students will get a full time employment with all the benefits of a usual employment in Sweden (health and pension benefits, paid holidays, etc). *Deadline for application: November 4th 2022.* For more information please visit https://web103.reachmee.com/ext/I005/1035/job?site=7&lang=UK&validator=9b89bead79bb7258ad55c8d75228e5b7&job_id=27467 -- 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/CALCpNBp_3CMobeAi0yoZqp6eG2_ea45UFSjf31X2zuZ%3Dnna_Ng%40mail.gmail.com. --000000000000292f5d05eb42406e Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

The logic and=C2=A0types=C2=A0group at Chalmers and Gothenburg university is now recruiting=C2=A0<= b>four PhD students=C2=A0to work on dependent=C2=A0type=C2=A0theory for mathematics and computer science together = with Prof. Thierry Coquand and others in the group.

The project is ab= out homotopy=C2=A0type=C2=A0theory and univ= alent foundations, where=C2=A0type=C2=A0the= ory is extended with univalence and higher inductive=C2=A0types. The selected PhD students would be working on topics = ranging from theoretical studies of models and connections to higher catego= ry theory to actual formalisations of mathematics, but they could also work= more oriented toward implementation of proof systems, in particular connec= ted to Agda.

It is worth noting that the selected students will get a= full time employment with all the benefits of a usual employment in Sweden= (health and pension benefits, paid holidays, etc).

Deadline for a= pplication: November 4th 2022.

For more information pleas= e visit=C2=A0https://web103.reachmee.com/ext/I005/1035/jo= b?site=3D7&lang=3DUK&validator=3D9b89bead79bb7258ad55c8d75228e5b7&a= mp;job_id=3D27467

--
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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CALCpNBp_3CMobeAi0yoZqp6eG2_ea4= 5UFSjf31X2zuZ%3Dnna_Ng%40mail.gmail.com.
--000000000000292f5d05eb42406e--