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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 25720 invoked from network); 27 May 2022 17:57:59 -0000 Received: from mail-lj1-x23f.google.com (2a00:1450:4864:20::23f) by inbox.vuxu.org with ESMTPUTF8; 27 May 2022 17:57:59 -0000 Received: by mail-lj1-x23f.google.com with SMTP id k8-20020a2e92c8000000b0024f249d1770sf1456271ljh.23 for ; Fri, 27 May 2022 10:57:59 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1653674278; cv=pass; d=google.com; s=arc-20160816; b=tz0BFZPpAueUukEzDenaf/2+MPNR6DbF52cLG5j1rDVPF/KuUVrVNG2tZhKEJpp1gT BTHuFVoZpEC6e+K8+DEJ+el0+vS4falpfad2p7VPh5BBTQlpV4LV0PYp+cgiGgsrwRf7 jpti8aIRVenivM6no4PhmTvwpZvHAU8PSrEboPS8QQ7KhbSNoaIKiveWRnBCveK4Inj+ WtdoIm32LuCYjkJyC8Y361xKJcbpiYuPB3XwZLlg+j8YdnzFJgpuKeWEX3a/q6PMlCPi jQAjhI6ONZXN5rL8CDXBcuCdZAR98r33TN1wtLOvZ6L53mVnipExNz6f73n2ulirAQ64 stsg== 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:cc:date:message-id:subject :mime-version:content-transfer-encoding:from:sender:dkim-signature; bh=0/TbcIiHD0e0Y/d0r2cuVie7oiPz3Aw+mU4z4AW8SHw=; b=QwTBjP5SvOV4Z3CivjFrlvrlh/xNI+OU0bjPy4lOF5Cl8IZwhOGhyixIfQ9rb9MM0J vKTDPcHDj6g4GLN6KVZj823u+GczRdPZOf20nJNr/jc1F00sqg+vVKaxVvAAFr2Ac2Qd L+eMnYNNLG7h/wXYHTmwo/KXFlG/NyMgzNIdmZLc8yYL1OcDjnNpFPRN9QeEkoUVfwk4 JaecuTl1spLYKKfHCr7lhnvelVJgIBMJhUvt9DBmp1GtLBjk4cU0yr+3q7yeW3wOkFEY XxXSy3lIpkHLWVMPMlFzbnrCkexPnUnH6uAAIk9HWfQ/Nv3H4m2fm4UG3NLO/a59Vljj 9QMw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cmu.edu header.s=google-2021 header.b=PvuBLUoU; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2a00:1450:4864:20::330 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=sender:from:content-transfer-encoding:mime-version:subject :message-id:date:cc:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=0/TbcIiHD0e0Y/d0r2cuVie7oiPz3Aw+mU4z4AW8SHw=; b=sXP+IjhitSPaY6r8iSbSoAfUfgiKNQ7Y6ShDSxvx5jwcYpPYKFWeP7gU8G5dlAMNR5 475T1K/4IWo/+Uwh5pZaqhFtTxZuAeN/UHi3q56cme4N9Ci3aWksSfhx2Zn+0D7ufJWp NlUSx/zrVYnE6Dqwx7Ghr+Zzzz+PCQ2Y8nCDgPvEAF5N+NDe09g5a8IGBQq5OLxYD1FD hkqg648+MJGDIv+8uNrYB5ke+i15QkeGgEZsWitymF7UoYqSMQTwRfo4yWDvuZIAGA1R +9dHnd3gLPu0bRMPVKNXF/YFoppY/lnc+CwHSZG1mx1jEzFkL70/A9SChlnibti9wl1m Bgcw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:from:content-transfer-encoding :mime-version:subject:message-id:date:cc: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=0/TbcIiHD0e0Y/d0r2cuVie7oiPz3Aw+mU4z4AW8SHw=; b=bOExjrctsX11gJm1kpuP+EJLyCk+XMNWNmACMfL/SxtRLikEUQW5+nYdK2Yi5IEV8d tOK7cpmmff3+ZNNVbeOXH2NW2xxj1eSGOafi2STRcme1wqdua6nwPBoMjth2tl/srAKo fG+LteB7Med61PUb8QsDs1dkkNefq1TNEuTFTrkdm9BLcpWRaaPdVcOPaNL7BCbZuuz+ wMLvuFP8l2tITtJaY+XqDbC7ZD26uxMTFA7/OML/wH7SN1E2KWBQcK8J4RHor7ZUA4Fu 0lRARVjXyWdOP+adh2FV95BOHDW8ENOkE9OK2+/hBoCeHy6o1DimkhorOfUZ4EDkKQUQ /fBg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM5325C97bvUoCM0k9LKWEFZx3DfHWvAyeaPWYcORP/18gfKy/bo60 bcgFDB8lWV4mik9T5Dtnb+o= X-Google-Smtp-Source: ABdhPJy45n4uGamPxoIJrb/tVKHQ1sjmuCj0cWBkieqIwOTlViwYb+G9LNtlb/+xDAPyakE8xigndA== X-Received: by 2002:a05:6512:22c4:b0:477:cc26:c729 with SMTP id g4-20020a05651222c400b00477cc26c729mr28461261lfu.315.1653674277922; Fri, 27 May 2022 10:57:57 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6512:10cb:b0:478:7256:822a with SMTP id k11-20020a05651210cb00b004787256822als1710675lfg.3.gmail; Fri, 27 May 2022 10:57:54 -0700 (PDT) X-Received: by 2002:a05:6512:3f88:b0:477:c0fe:3383 with SMTP id x8-20020a0565123f8800b00477c0fe3383mr30734792lfa.3.1653674274479; Fri, 27 May 2022 10:57:54 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1653674274; cv=none; d=google.com; s=arc-20160816; b=xTRiI2DCRRX/tgJCfl7DHCqH124D0fOjIc+7GieHfK57NpkcMVvbeCfdQIgoZTeX8f /jY6Xm58+d71UOVC/HQOgXs9mQmNuih/PezhjK4xc/Kq23AEZ3UA3yO97a+ZpKpv++d8 m20Ee2YF/L35fLM3DkPT/AVfMEkvv1eXJUirBYwCXsb5XoZKGWJxF4XDnHyZ6v/6TFEk 9iw0wMQ1k/7qQhsW/UivyCTEHpxgXexnkISt+W4SlWHF4heLq8JW0TA0Gho/UerWWZEh N3G6RoCLfKx7O8G83rWltqqohJX3es+RtbTGp7smcRbnv5iHzCQ1zoO2ZvIanLJZnaVj gJ5w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:cc:date:message-id:subject:mime-version :content-transfer-encoding:from:dkim-signature; bh=6SxHgWmz4jXtFdMI7F73VVOG33i2XhrjhoCFTXddcnY=; b=UTwcArxaow6ddp7u67sQLH6RrBJanxS5sCTyEuO69FLVX+G71dSocwpORvF3lVnYa9 Xo4xnbPCKx7PT1ULNoTh3smer8/FTYbFx15RSQZeL7u0ATiCiq1WueF5izR9KhEekDjl LPKrpyq3I+8wmxzy/umvVYjaMR7Mm4plp62wxzbJO2dEm0QVKa2KII0MUmIcLekc53ET a27HzfGnmUfREfPIdVwyIHK1JsfIJsqclLTiJrMEkyCnre8hAc7saFLPj/cGJ7hzrk07 qRlDaTTi2nv/cymbmWdI4lgJpmMvwGt4FLPLYK72P/MzR+kHOCC108Ej01f/PbCW8XUl Wepw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cmu.edu header.s=google-2021 header.b=PvuBLUoU; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2a00:1450:4864:20::330 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: from mail-wm1-x330.google.com (mail-wm1-x330.google.com. [2a00:1450:4864:20::330]) by gmr-mx.google.com with ESMTPS id v12-20020a056512348c00b00473a659879csi245484lfr.13.2022.05.27.10.57.54 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 27 May 2022 10:57:54 -0700 (PDT) Received-SPF: pass (google.com: domain of awodey@andrew.cmu.edu designates 2a00:1450:4864:20::330 as permitted sender) client-ip=2a00:1450:4864:20::330; Received: by mail-wm1-x330.google.com with SMTP id c9-20020a7bc009000000b0039750ec5774so3117916wmb.5 for ; Fri, 27 May 2022 10:57:54 -0700 (PDT) X-Received: by 2002:a7b:c183:0:b0:397:4924:7cfe with SMTP id y3-20020a7bc183000000b0039749247cfemr8154820wmi.128.1653674273817; Fri, 27 May 2022 10:57:53 -0700 (PDT) Received: from smtpclient.apple (2a01cb0404e03a00853cd9c51ff9085b.ipv6.abo.wanadoo.fr. [2a01:cb04:4e0:3a00:853c:d9c5:1ff9:85b]) by smtp.gmail.com with ESMTPSA id n21-20020a05600c3b9500b003974860e15esm3306740wms.40.2022.05.27.10.57.53 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Fri, 27 May 2022 10:57:53 -0700 (PDT) From: Steve Awodey Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3696.100.31\)) Subject: [HoTT] Autumn school on Proof and Computation Message-Id: Date: Fri, 27 May 2022 19:57:52 +0200 Cc: CMUHoTT , schwicht@mathematik.uni-muenchen.de To: Homotopy Type Theory X-Mailer: Apple Mail (2.3696.100.31) X-Original-Sender: awodey@cmu.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@cmu.edu header.s=google-2021 header.b=PvuBLUoU; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2a00:1450:4864:20::330 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu 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: , Autumn school "Proof and Computation", 26th September to 1st October 2022= =20 https://www.mathematik.uni-muenchen.de/~schwicht/pc22.php An international autumn school "Proof and Computation" will be held from 26= th September to 1st October 2022 at Aurachhof in Fischbachau near Munich. I= ts aim is to bring together young researchers in the fields of Foundations = of Mathematics, Computer Science and Philosophy. Scope =E2=80=A2 Predicative Foundations =E2=80=A2 Constructive Mathematics and Type Theory =E2=80=A2 Computation in Higher Types =E2=80=A2 Extraction of Programs from Proofs Courses =E2=80=A2 Steve Awodey: Categorical logic =E2=80=A2 Marc Bezem: Coherent logic =E2=80=A2 Hajime Ishihara: Reverse mathematics in constructive set theory =E2=80=A2 Klaus Mainzer: tba =E2=80=A2 Stefan Neuwirth: The philosophy of dynamic algebra =E2=80=A2 Fredrik Nordvall Forsberg: Universes of data types in constructi= ve type theory =E2=80=A2 Monika Seisenberger: Extraction of programs from proofs =E2=80=A2 Chuangjie Xu: Various approaches to computing moduli of continui= ty Schedule Monday Tuesday Wednesday Thursday Friday 09:00-09:50 Awodey Ishihara Bezem Mainzer Seisenb 09:50-10:30 *Coffee* *Coffee* *Coffee* *Coffee* *Coffee* 10:30-11:20 Bezem NF Seisenb Ishihara Neuwirth 11:30-12:20 Neuwirth Awodey NF Groups =20 15:00-15:50 Ishihara Xu Neuwirth Awodey =20 15:50-16:30 *Coffee* *Coffee* *Coffee* *Coffee* 16:30-17:20 Seisenb Bezem Xu NF =20 17:30-18:20 Xu Groups Groups Groups =20 Working groups There will be an opportunity to form ad-hoc groups working on specific proj= ects, but also to discuss in more general terms the vision of constructing = correct programs from proofs. How to get there The default arrival time is Sunday afternoon, and departure time Saturday a= fter breakfast. There are frequent direct trains from Munich Hauptbahnhof, = departing (at tracks 27-36, Bayerische Oberlandbahn BOB in the direction to= Bayerischzell) for instance 15:05, 16:05, 17:05 with arrival in Fischbacha= u at 16:13, 17:13, 18:13. From the train station in Fischbachau it is an ea= sy 200 meter walk to Aurachhof; see its website for directions. Applications Graduate or PhD students and young postdoctoral researches are invited to a= pply. Applications (e.g. a self-introduction including research interests a= nd motivation) should be sent to Chuangjie Xu (xu@math.lmu.de). Students ar= e required to provide a letter of recommendation, preferably from the thesi= s adviser. Deadline for applications: 7th June 2022. Applicants will be not= ified by 20th June 2022. Financial support The workshop is supported by the Udo Keller Stiftung (Hamburg), the CID (Co= mputing with Infinite Data) programme of the European Commission and a JSPS= core-to-core project. Successful applicants will be offered full-board acc= ommodation for the days of the autumn school. There are no funds, however, = to reimburse travel or further expenses, which successful applicants will h= ave to cover otherwise.=20 Klaus Mainzer=20 Peter Schuster=20 Helmut Schwichtenberg=20 Last change: 27. May 2022 --=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/F25F51B6-568D-46EA-A29D-3D118B7DD77E%40cmu.edu.