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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 27889 invoked from network); 5 Jul 2021 19:36:38 -0000 Received: from mail-ed1-x53c.google.com (2a00:1450:4864:20::53c) by inbox.vuxu.org with ESMTPUTF8; 5 Jul 2021 19:36:38 -0000 Received: by mail-ed1-x53c.google.com with SMTP id y18-20020a0564022712b029038ffac1995esf9605137edd.12 for ; Mon, 05 Jul 2021 12:36:38 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1625513797; cv=pass; d=google.com; s=arc-20160816; b=Mky1IakDlp2UY2k/i+hYqqE8cONJgf+eqL20N+L5CxxR0PGe8isCGAIiki4c0799q7 YbD6wTQExS5p/NAXRmUCM5LcREUR7TDlxp7Zy+1oMxu2WhbDIExUtsJ13OznGPnI4M0y q63J/LZWHTeM2q1sG5T9WbyyX5lrhDLNQc6V5rKfCFHyikfTVbEie7oHX9tS+nANG1OM 1w0i8wPfY+Htt51QbRjdCPxc4K5ELT+RelM22rQMWMMnKhKpSbLlWyYFUtgujZ7yKqdO RA2BPbpNFStpNqomxiZ9FwLM1bhfWU32QL7KqOtSqeXD9Fv4IVTqensDd2gNXals1ACu XZsQ== 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-transfer-encoding:content-language :mime-version:user-agent:date:message-id:subject:from:to:sender :dkim-signature:dkim-signature; bh=JtG/dY/L1J73RWIWyWrKtNM9skuYuxtjWAxbjHb/ofA=; b=RL2G/ivjYteRXc7jBCoYqYt1nmh174tV1u91DWF2AapVQW/6IMFyXVfHzB+PjOgFxx yvEwZ02G1IFj78nWXGJ84IU40HDnK7TDitbirgavXVOQMHVnlQwh+Y75V2/VFXY7bKC5 KUzEgKoHImSSEkZ8gh9dvYYyJss8fnWomqkynU/3P8ejKsn1pPP/zypMt1ISzXQ39vs/ 4ENNa5Ut9/+Pj/TLq4E87Ln0c3TQAlpaP8Ty0kKw1+ZLmKn4/aJb48T2Q8MZx9hS/X4P e8lH1LarY8bTwFZ7ykxcx+Zp8dvPwtJBz0LLpx9h5mXHlk1EbC0l7LnzuRiKj7LyEfO7 jpUA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="CG/WDG8t"; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::430 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:to:from:subject:message-id:date:user-agent:mime-version :content-language:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=JtG/dY/L1J73RWIWyWrKtNM9skuYuxtjWAxbjHb/ofA=; b=joeWBjtCdsHuhZqjDqJ4lyENpQYXBrw4npt+9G3o5FUevVI8E0QiWNLmRRKtAJkmub b7k69ao4SlwBvxG6lkkhZ8It75rzltBvemeLqMvOzI4NVdMLWmFHcjQovrWlCCCTHjGQ KQ56szfFF1TzE+SMfPfjBoVr86g8KjEmM5qEcxkoS9nPG7z+m90dXcUCSmnTRL82bN/k 6z+5hrXdsRWxemAs/Pbz7PzcIaVk6xLCKX9MCnXhbFkmiJiOp9YfUY9d/GKncJ/JMVnB 98S9Wz7YL69AbNGRMsusyQknx+2x8Ge/Tpy8svLdOX4s/KOKNTC/ACBf7TvpbCd48KAK I/2Q== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=to:from:subject:message-id:date:user-agent:mime-version :content-language:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=JtG/dY/L1J73RWIWyWrKtNM9skuYuxtjWAxbjHb/ofA=; b=qP5RevVOk9dBJOUUw25F7oaVJ42i0CcnaN/nyk6roNqkNl7kmqHeQ6wwoiiRjHgZ99 WlsZOV6N9pM50qrVXuoFP6PqRTdbAuPJrS1ho/92MRt16JEPzpXplYlVF4ymYPE9e6dE fqy0p8od2rvnHo4w3OrL1pz+u7exnnfTMReh+wjQBxv0k8ertKeN3FM5boi3Eq2x2OiA RazD9Uc+Q3cJtEtAs61fZeqkvO0V15wqaII+dw6ICo6ZLAfo0lBZbAiOGwfXGdbV3ql6 gIBlQuO8LvGHCacwYuVif9JasGYxEAHd9v1ayMkBq528W3MUr19YGL41MMRFN3foPBFv uPLA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:to:from:subject:message-id:date :user-agent:mime-version:content-language:content-transfer-encoding :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=JtG/dY/L1J73RWIWyWrKtNM9skuYuxtjWAxbjHb/ofA=; b=YNS2/sDopH4uLsL+OVSMX4iu0a0R+w5TqQ6widW1fjev/EcMx81w5lL42ugvd+V993 nYkxeLwIQR24PiFDIYwfEJbibiE8wWY8oSwPQb+TbGPlMTQ+wJzE7iWSvHO9WEanAssI AfKpXpSJy1t1+hI2Dzsqbuu3Pn1XmxzSHL63HrGZ30KUVk27Uy4oprCvNLPOCNaDlZqt Z6PyZ4fcIC5V4cs/Z+re9Ron5+kCBBkoIdRI1OAM6tOP5O/28zYml4jHMsHjTYJly3M9 iYuDzihENp0nIkRuL3x+AJ37jMDnu+PyqiGytOn1mILbe97+rycBtSoGlGKcBN0leJBt NP7w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532z3TSzkPUZL0dLV+jiww6F5UkXyjrmGQPiFoKn8wA3EZrAJzBI hIyMrqvwGVsDbeKJigC7h3g= X-Google-Smtp-Source: ABdhPJzWs0UgmT9pA7w9uG+uReR+ETPmYnsj81+T6vI6w9SsWOvokH+lcbuPz+C7RVJeGJilRGIK4Q== X-Received: by 2002:a17:907:2ce1:: with SMTP id hz1mr14302622ejc.376.1625513797372; Mon, 05 Jul 2021 12:36:37 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aa7:d905:: with SMTP id a5ls7409512edr.3.gmail; Mon, 05 Jul 2021 12:36:36 -0700 (PDT) X-Received: by 2002:a50:ed82:: with SMTP id h2mr18055738edr.165.1625513796454; Mon, 05 Jul 2021 12:36:36 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1625513796; cv=none; d=google.com; s=arc-20160816; b=Tz1Fu+pwyzXkqq926INIQD8wCCuQ9TfHxowPsPzRrDrPDyngBjebFGEHbMWmwbfeG7 65LRp6iFCIImAxc4ifqg0hPVpda43itnaDnDI2RTt1Akoiz6gC8fLckSLxmXuaUejkuB 3cHcS1d3Cw1+/jPp8Yas+vcEOdbmBf0AawtWT5xUaZ6TGoeVmD6qZpsJPXkRrFNh6HQA wxyPBOUh50oCIQcKXkazO30eD054y8RnzB/qts7+BMhNgGP8aQVhwDBb4jYLY69eKFvQ wUP7mRFrodOIll4VzuDexxoYOe7CgVn2Xfjv911vGDltfyMPBbXS6ifY9hTzVqXQXWQ0 UBsA== 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:subject:from:to:dkim-signature; bh=tZAqlTZRGegtwrAqO/Anbq9CuoBjtUfBpJEhCbp8he0=; b=bEuP80f0+TGOYRQEQFqvGAAqr4nrTWkur7A+tbZNZt3rc1cp4bVuUyzbajLHnTVUMc IbdQeF3ZSluVtX0xpnuIIku7oUa0ozzHb/AKfWFXGorQfAw9A7vCz/BgtEgsuezivc29 f9Z6kW4NkeQPgByjX4Vmsgfgb7OTep1G4qknRh6TMKQrGs+k8kXsU2UgpyZlMZENSPQ/ vFaIJCeHkj08MeinqJg764gAiVdy24Ob9UaPNKU+pKtCJWyj9hz+fdxX44vEaIlzFJ96 IYH6O6Z/Lcdkd4EbUuRis0ECvgR3Qf4Q17lsQcPj9NZaFc6bkaUhC18w1USn6kbcCY3V sOMA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="CG/WDG8t"; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::430 as permitted sender) smtp.mailfrom=benedikt.ahrens@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wr1-x430.google.com (mail-wr1-x430.google.com. [2a00:1450:4864:20::430]) by gmr-mx.google.com with ESMTPS id s18si453454ejo.1.2021.07.05.12.36.36 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 05 Jul 2021 12:36:36 -0700 (PDT) Received-SPF: pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::430 as permitted sender) client-ip=2a00:1450:4864:20::430; Received: by mail-wr1-x430.google.com with SMTP id u8so23260417wrq.8 for ; Mon, 05 Jul 2021 12:36:36 -0700 (PDT) X-Received: by 2002:a5d:4849:: with SMTP id n9mr9912602wrs.186.1625513796117; Mon, 05 Jul 2021 12:36:36 -0700 (PDT) Received: from ?IPv6:2001:a61:1305:a101:4e49:5913:4c5c:b2e3? ([2001:a61:1305:a101:4e49:5913:4c5c:b2e3]) by smtp.gmail.com with ESMTPSA id l41sm435927wmp.36.2021.07.05.12.36.35 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 05 Jul 2021 12:36:35 -0700 (PDT) To: homotopytypetheory@googlegroups.com From: Benedikt Ahrens Subject: =?UTF-8?Q?=5BHoTT=5D_Conference_for_the_90_years_of_G=C3=B6del=27s_Incom?= =?UTF-8?Q?pleteness_Theorems=2C_with_a_session_on_type_theory_tomorrow_=28?= =?UTF-8?Q?Tuesday=29?= Message-ID: Date: Mon, 5 Jul 2021 21:36:34 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.11.0 MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US Content-Transfer-Encoding: quoted-printable 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="CG/WDG8t"; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::430 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: , This week (5-9 July) is taking place a conference to celebrate 90 years=20 of the publication of G=C3=B6del's Incompleteness Theorems. https://uni-tuebingen.de/en/einrichtungen/zentrale-einrichtungen/carl-fried= rich-von-weizsaecker-zentrum/veranstaltungen/celebrating-90-years-of-goedel= s-incompleteness-theorems/ The conference is composed by a series of workshop: - 5.7. Monday afternoon: Opening. Higher proof theory after G=C3=B6del - 6.7. Tuesday morning: Type theory in type theory - 6.7. Tuesday afternoon: Computation in face of incompleteness - 7.7. Wednesday morning: Cut-elimination and Herbrand's Theorem - 7.7. Wednesday afternoon: Provability predicates - 8.7. Thursday morning: Diagonalisation - 8.7. Thursday afternoon: Recursion-theoretic approaches to computation=20 and complexity - 9.7. Friday morning: Philosophy of mathematics after G=C3=B6del - 9.7. Friday afternoon: Aspects of G=C3=B6del's unpublished work; Closing= =20 Lecture by Jan von Plato If you would like to participate online, please write to Marcel Ertel=20 events.cfvwz@listserv.uni-tuebingen.de to receive the Zoom link. --=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/c37ae81c-d30c-b69a-9e04-934373a4214d%40gmail.com.