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.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 10880 invoked from network); 25 May 2022 06:51:20 -0000 Received: from mail-pf1-x43a.google.com (2607:f8b0:4864:20::43a) by inbox.vuxu.org with ESMTPUTF8; 25 May 2022 06:51:20 -0000 Received: by mail-pf1-x43a.google.com with SMTP id x21-20020a056a000bd500b005188ce4a068sf4056802pfu.17 for ; Tue, 24 May 2022 23:51:20 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1653461478; cv=pass; d=google.com; s=arc-20160816; b=HFbLDKR5k/fgFkNq4H9ClDv+lr1ruz2YHA69ocfYHeuolkUFcoP+6thE8RzFq6803m UIE/Q59PiW9OXecS/eXOV+Y8n4O49le2b7mNwzkqgbWzpMu22Ja8zOTDp46ElytYMNa8 lORSGycQHZq1RHB6YYgWfY5tlpkP5nvxPXfS1cw/B9VAb88x3czgZYhZSbvZWYAj3h6e 0q0z0u1uFJXIcva9IcWhq98tDyFXrmcAY6VkBWMNgEIbVbQqt2U96IraWaqDxUSJEK0+ IeytvIylcoZYcWGQc6qEGn8uhB6jE+EAR02fo4MxBrh/NUonBJyPhmnsZd7oXgfIZihS ei2g== 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=ddpC03yo6g3fh+1mk6K+rus7qolhRWByUN/VCDF/IRs=; b=Eo+JyXpjr5vCCuRUzkg16/yrNoV37kk3B7WsvRa4PJd012siWwn1Cbc/dK667DfMXJ afLLqCTwnhGtnwEZLcjj9gaE3HFZ+ulo9ac3qjhyPAfJAOcfIeX577O1IB7f2LDTyZmZ LGlRW+I8jnV7/JuuciJhMGgh/SljJ8N9qq9pjnYUlc84t2TE7Ueqi61TCwGQOfuBQi6v Sbb6Mg2X7n/NACXRer1i5oQIgVX9QhhRiAfJ6ZZPQrSlpTlplM9y//cMNMxryzRxl9pY ejoiqTgvIUNQx3Om9rxJoO0sgDGNLuRLE7k+uM4gO2swQRmvZFghFf/oyveq2wrZ1yAk 17HQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=kMsrwGrW; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::a2a as permitted sender) smtp.mailfrom=andersmortberg@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=sender:mime-version:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-subscribe:list-unsubscribe; bh=ddpC03yo6g3fh+1mk6K+rus7qolhRWByUN/VCDF/IRs=; b=DeUA7XXN93ZjAeiS70eDEkiC6HRCIX7kGI/XqRL9yaMGHohDjMF50B9IbplsDzCy9t 5di79O6kobk+hB08+8hQDRuhFUZS8ccR6R6T1ae6+jR/ZXFZ07yE3W0CFhvsCOkhiKLt 0cPXY3kUMjrrkHmEhMSLF/DOHaTpwUW5/kda/9Bq/ReV0H8CWkWC4vtsebWOT/d8MlXZ ZZrjCXeEEZQ33H6mshogjmq0sB4ZRh1h89yBzdsVSID7oo2CwP+NAoPOOSztugeefWjb m2esNfSHEpoZEZatpMYQTaI3Xqic60Ulzz8sG7hqRHR54+ksY4a3jFo/iRmklo8xS93P d/2Q== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:from:date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=ddpC03yo6g3fh+1mk6K+rus7qolhRWByUN/VCDF/IRs=; b=BlQZ4ihhn+yXSy0WNWkce5oBqORz0NkCqDPVpE2nYVpnQXAEp5nxLWTLZymaHOPgrU Q4HIqaxJ4oa9mQgUc7a0XBF8C/LmvyPy31Il/S5rjXqH/NyMDynqUeBPGux9KYM1ifwm e3witnGE6QI+110h4u+hF2lHK0tWfoDIglv6cmktlvc7qg0VhTHFe67b4ZhUbU8J/0R6 AypEkkf5Ni2xWrhkSNBLuDEX0yxaw+b/PEh5evEk2/FSQQbQIbFwHGPib1MbvRBFlzFA t+sWURRrK9hBm+zoNx6WFtoc/EfSNeNFqePiw1paMcAE2DyRJpN357gy4y1vCc98YViV YK6g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-subscribe:list-unsubscribe; bh=ddpC03yo6g3fh+1mk6K+rus7qolhRWByUN/VCDF/IRs=; b=ZmUs1LyxZmeUSt1vwytpnwJ329osHBugmXpyYZhQmlyoI2X2dspPPgZVD7PzOJ4brO 1jzMxGr5NjnNplIwTbA5Q3Se0dTsseY65qkCYudOKWDR1M+rJU8XhV55cs6uLyriZo1D eorLM9AJtdtgi7bPDyUyeYotr0nM3mCFWrqRy8AuPZPVjhKN6BoFBiGm4naSxYkgT6xo ejUT+qUE6P1+yTncNJMEatLmtApGOTRtTwjkFT3i/JxrjEDxy46rZx052T/Hq/yo3VvH i/xyj0Sw4SCGtSBoyTxQxp90mc3eBER4TGo92Grrzu/MzvBhVP8X8J+0UxuwU+dyqVAk PIUg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM531gR1cOtlndIFuvLLiSbLQlwVnb/pkrQE29XQPS/Lb7ycSwv8xS 6WZECb9xlaBa2AMVQoYtr/4= X-Google-Smtp-Source: ABdhPJwzdoIVqsnNWGMefMFRKd18FfQFt0udjaEHe1QM53P2e7oi16IYeQb+X2qD//lz+4dRLXsPOQ== X-Received: by 2002:a65:63c4:0:b0:3f6:3a63:3148 with SMTP id n4-20020a6563c4000000b003f63a633148mr25640019pgv.33.1653461478014; Tue, 24 May 2022 23:51:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:244:0:b0:382:b131:96eb with SMTP id 65-20020a630244000000b00382b13196ebls7073337pgc.3.gmail; Tue, 24 May 2022 23:51:16 -0700 (PDT) X-Received: by 2002:a63:535c:0:b0:3db:69da:1ef7 with SMTP id t28-20020a63535c000000b003db69da1ef7mr27925620pgl.239.1653461476357; Tue, 24 May 2022 23:51:16 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1653461476; cv=none; d=google.com; s=arc-20160816; b=DLfNY6Z+FPw2zqLIWDpQ4ZBCQ09TskBf4cZsDiycdKwR5Rv/wICdDrKYqt50Lu/CFU TJTL284hv558seC2oDI6lkXoApa0bGAABUIlkeyYdBGx5WQXRyKjD37mISZkNuMrXsZ6 Da9UyLSH8j4JqyMQANNQp+yxd0o+KBSGXVCIqGJLB6GI2XYUH7UezCt8HXlamODk0nH5 9Xsd2kvD7IVIsG9EkyIKuX4VazVjA+LDp3SeYvFIRm7eKRRuT7QkIK2IXNjreYnsICsr mPMvQw91tvlp9pC0NeZNpuBaUn42xmfvZX/E3TU1bwqBa3mjFqerykz9CqCMXFVUZ5QF XChg== 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=PZVHu8Tlgi6MDkSZ4qp8/Ib5PMzKNB+Ac1xfl8REfZs=; b=hUubIGUp076vb/R7mVy0lk6NqRKbq6TbuBXqcrKVcQIwbjEVPjIzpcVFiCf1+IX/fr Vn1vlMCUxxvIWAo9LjE7yGq9fWuYs1u/5Q/2vPid5IUIrskTm0753o5GOwzDX0KDduUS KKoNrmBjqbERICqAKL3UsyCIyWFvOcNY0MvmMTnADdDym9DW+rLICN5NJAV7lPVvttJp dbdJUiDQqkDCZ0rKGQPqxLTnj5DUz4xRWLQi3Z9FOvyUvUnmwsCOf8LPpoeVQhmBQaLE abi1ibqkzW+C7GKigsDnV0X11F1Je0W0dcrOVT4OPlAjhhvbx8PykVIbxS5b/xdbIkFG ttDA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=kMsrwGrW; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::a2a as permitted sender) smtp.mailfrom=andersmortberg@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-vk1-xa2a.google.com (mail-vk1-xa2a.google.com. [2607:f8b0:4864:20::a2a]) by gmr-mx.google.com with ESMTPS id lr15-20020a17090b4b8f00b001df25a64c1asi190857pjb.2.2022.05.24.23.51.16 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 24 May 2022 23:51:16 -0700 (PDT) Received-SPF: pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::a2a as permitted sender) client-ip=2607:f8b0:4864:20::a2a; Received: by mail-vk1-xa2a.google.com with SMTP id bc42so9444209vkb.12; Tue, 24 May 2022 23:51:16 -0700 (PDT) X-Received: by 2002:a05:6122:2022:b0:357:66e3:828b with SMTP id l34-20020a056122202200b0035766e3828bmr7309774vkd.34.1653461475325; Tue, 24 May 2022 23:51:15 -0700 (PDT) MIME-Version: 1.0 From: Anders Mortberg Date: Wed, 25 May 2022 08:50:38 +0200 Message-ID: Subject: [HoTT] Workshop in honour of Thierry Coquand's 60th birthday To: constructivenews@googlegroups.com, Homotopy Type Theory , coq-club@inria.fr Content-Type: multipart/alternative; boundary="000000000000e3004e05dfd07fc8" X-Original-Sender: andersmortberg@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=kMsrwGrW; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::a2a as permitted sender) smtp.mailfrom=andersmortberg@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: , --000000000000e3004e05dfd07fc8 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Thierry Coquand, professor at the University of Gothenburg in Sweden, had his 60th birthday on 18 April 2021. We are organizing a scientific meeting to celebrate him and his seminal contributions to mathematical logic, constructive mathematics, theoretical computer science, and the development of proof assistants for type theory. The celebration was originally planned to take place in direct connection with Thierry=E2=80=99= s birthday, but had to be postponed several times because of the pandemic. The meeting will take place in Gothenburg on 24=E2=80=9326 August 2022, and= is open to everyone who wants to join the celebration. It is free of charge, except that participants who wish to join the banquet in the evening on Thursday 25th of August have to pay their bill directly to the restaurant. Participants are also asked to arrange their own travel and accommodation. For more information about the meeting please visit the workshop's page at https://tc60.cse.chalmers.se/ If you plan to attend the meeting, we kindly ask you to fill in the registration form (available from the link above) by June 30th at the latest so we can plan catering and dinner. Sincerely, the organising committee Andreas Abel, Ana Bove, Peter Dybjer, Peter LeFanu Lumsdaine and Anders M=C3=B6rtberg --=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/CAMWCpp%3DTCM3q6wocdqfn-2LyfegSaNqmdOJ%2BzVwfJ14dGQbjRw%= 40mail.gmail.com. --000000000000e3004e05dfd07fc8 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thierry Coquand, professor at the University of Gothenburg= in Sweden, had his 60th birthday on 18 April 2021. We are organizing a sci= entific meeting to celebrate him and his seminal contributions to mathemati= cal logic, constructive mathematics, theoretical computer science, and the = development of proof assistants for type theory. The celebration was
originally planned to take place in direct connection with Thierry=E2=80=99= s birthday, but had to be postponed several times because of the pandemic.<= br>
The meeting will take place in Gothenburg on 24=E2=80=9326 August 2022, and= is open to everyone who wants to join the celebration. It is free of charg= e, except that participants who wish to join the banquet in the evening on = Thursday 25th of August have to pay their bill directly to the restaurant. = Participants are also asked to arrange their own travel and accommodation.<= br>
For more information about the meeting please visit the workshop's page= at https://tc60.cse.chalmers.se/

If you plan to attend the meeting, we kindly ask you to fill in the registr= ation form (available from the link above) by June 30th at the latest so we= can plan catering and dinner.

Sincerely, the organising committee
Andreas Abel, Ana Bove, Peter Dybjer, Peter LeFanu Lumsdaine and Anders M= =C3=B6rtberg

--
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/CAMWCpp%3DTCM3q6wocdqfn-2Lyfe= gSaNqmdOJ%2BzVwfJ14dGQbjRw%40mail.gmail.com.
--000000000000e3004e05dfd07fc8--