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_FONT_FACE_BAD,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 17782 invoked from network); 5 May 2023 11:06:14 -0000 Received: from mail-il1-x137.google.com (2607:f8b0:4864:20::137) by inbox.vuxu.org with ESMTPUTF8; 5 May 2023 11:06:14 -0000 Received: by mail-il1-x137.google.com with SMTP id e9e14a558f8ab-32f240747cdsf104379305ab.1 for ; Fri, 05 May 2023 04:06:13 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1683284772; cv=pass; d=google.com; s=arc-20160816; b=RywxLOMo6ywLhEb6vvFQ19nZPi846E4EK7O7CNEictx+T0tBPcnXTsOf7Fc+fBNH5r j9eShnuXQTcXpzARmEPCXf0TzQtT0/umQHXyEQcmtIBwhOeJ+/Sp7pZ0SDWFsjTZVrlg NC35x2UG8XmeJ16dKFLV63bJxC21gr+yhvylrNEIt0VCXU75xyF0+tmFUN29gG2vPQfu DZI0zJR+W+USR9Ezm9YkreF3EM/C8z4NpukqxMiTcZXNzoHbHk1rG/rYxQ92MIIz045e BLcmGN69S1rZ6+zpTWg+DNTkZ61Uv/fZeVw1GxgWedlbeOUK3sajAyyCc1rSgm22SZEb nEHg== 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:from:sender:dkim-signature:dkim-signature; bh=16A4X70qzxN+qIwoGnXrm74ctqblV+ZxxB10DKtXoXQ=; b=xPnRLKZTkwVXblUxWmLK8znlAFrY0tF4V52ZlZakCX0Y2GE6VXL7ng8XfyCY6CV4SP Kgdw5DU87twrOt/b7HpZKnxzT5TWcIU3MvWn79oR4sprdeev4nIE+A/lH/8PG3zAwmss d0t0AF7AJcVAC5/EDlZirpJwak4GJMtZTzIvM9p6CrHcaI2i/pgga4VFFpZGm2YIQcKH YlrR3ukFn2cJMqeDE2tH3ItyzcRgC+Slk5mrfZB3zItS9eC4HFgljzP6NcgArGnAe/3m Rv+2o8sT2pkqPN3oPanj/Effp6b08J5Qtzljxl90L3DWNFrBFLpA9vIgE3cUV8yYlBxo So6g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=sSId7YSS; spf=pass (google.com: domain of steveawodey@gmail.com designates 2607:f8b0:4864:20::f32 as permitted sender) smtp.mailfrom=steveawodey@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=20221208; t=1683284772; x=1685876772; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:to:cc:date:message-id:subject:mime-version:from :sender:from:to:cc:subject:date:message-id:reply-to; bh=16A4X70qzxN+qIwoGnXrm74ctqblV+ZxxB10DKtXoXQ=; b=Z4hcLm1bgrJV/EVIMfUjakzA8oJBSKTWMDZeqBVYGmCZ4ZeUM9H+achwG49gxfe3JR 7RW0jdPMj+g8z/sZ7dZk+ujJNGJIk+2zbzTlr/cVvDQIQ3DEy7Getpg4S2S4YF1mhWbm jq0TJw3ZIaDTxWC07irpeDOcIDoP/imGo3ZKTK8zEcxuPz5tq/QRuQyC3hHVIJSGTHTb eWhJhMN7L3E80EADQNCOn0TG6yrMH6foFw4xiAezHxvudhhpQ1sgPsu2O4fd4/oIV9NI eu80nb+5FTxCpnFf7tKpbdArLnPKsNKVgQX7gtEcyO9XaqHp2Jy2qj94MOqk/qJOyThx yEdg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20221208; t=1683284772; x=1685876772; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:to:cc:date:message-id:subject:mime-version:from :from:to:cc:subject:date:message-id:reply-to; bh=16A4X70qzxN+qIwoGnXrm74ctqblV+ZxxB10DKtXoXQ=; b=nf6rWsZk0C45enmn5jvnaLJ6afxmK6cFtK3UzxIqyEe8yuJ50UtRr9h9yCz4SXsZVQ k9TybRyQinwRZxgPL7zFTMAAPWLZiRxnVUQMbe4LZ751P9aBIM2ciPMFKwRRSTs9zQMq YI22rYBqVkrRzn3lO5PSwXpmJ+vATOYMomApmdYD8zOVdWxdhDwk/TyDEAu3reDpvbZp xTI/578VxufP4extYyOGGlhG+NLQgHSd/98wTo7NcLKZ0ikNzB34c1m9HyTIDLkOicqB plKDwmaSgRw8HIMqlXKLZMzULV143Rid7Ar+1KqYapv5MzP/JbDVAogOjdWc42T5ze8m oQow== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1683284772; x=1685876772; 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:cc:date :message-id:subject:mime-version:from:x-beenthere:x-gm-message-state :sender:from:to:cc:subject:date:message-id:reply-to; bh=16A4X70qzxN+qIwoGnXrm74ctqblV+ZxxB10DKtXoXQ=; b=BdBoUWDh0aPiOHpJaIggqNi5UU0cexmVUwxWaquLNLgd4X/I9seVFIC1HBG2SkIpRj MhN5O2spLYOIG+FdIg/6EOmaP/dUGr4S/qJRq5sc4TfRdIOMSe6vRo1FgqxILCGRDJFy qD+xA2VC9sE7Jml6lC5LFYRbPb8X8ccSKbFbFwCLZsy7lRtrZ4JNx3dizdLiWrMlyvs4 pkKpnRtXtE2up6LQjQiRPTXBvKtCvW7ZUSMJt07Ciqn98oTo7cVjqrhhNqv1Tz8M98k7 /qHHkPzoNaDq1kl5NTEJMYN8VxIMUS3F49oLZ+6ZpS/NguctFzmhDK714jR6TlxMl/pw Jsng== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AC+VfDyMJpn8XjR/AinIg/peIkxsaTmdY+yjzyq1TAz8i2CjsxOxWSmK 04Yn7+sx0SL1Mwkvx5Zu/Z4= X-Google-Smtp-Source: ACHHUZ6X1Yp/RYHJVTrkGmA6kLJpjNWQ8p1fGJ0eiv+qAz/7VJ4LqkkMcS31CHqEo6vqkcfIwr84IQ== X-Received: by 2002:a92:540a:0:b0:331:31d7:9816 with SMTP id i10-20020a92540a000000b0033131d79816mr1236150ilb.1.1683284771590; Fri, 05 May 2023 04:06:11 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6e02:2209:b0:331:2df7:644b with SMTP id j9-20020a056e02220900b003312df7644bls532427ilf.0.-pod-prod-02-us; Fri, 05 May 2023 04:06:10 -0700 (PDT) X-Received: by 2002:a5e:cb07:0:b0:760:f816:280b with SMTP id p7-20020a5ecb07000000b00760f816280bmr431790iom.8.1683284770050; Fri, 05 May 2023 04:06:10 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1683284770; cv=none; d=google.com; s=arc-20160816; b=aX3bgPZIRb4nrCnwU72gWSdb3Ou/KZxQkKlrSFIYQJp9YF1NTAqFWOf3RAQ+sg1mYN 0BzgQnwru9f5AmUof7fH0ap2Nws5btEW7gz5i7PB5dg/W0qX5uzIndUKQ9rb36j8J2FA GkzqcEV0s5hdLRYJYIO2EESGSka5OMRYAqXnLgTnNHcCoLjeyaHlflRgcpouX6ro98r9 2JG41tZHFnHambsse/RoCjNtyXSKBMzrRgFjAgT0eou3IjR0y7+CgxhyFwBdm/5fB9Bs Q6pcfKKKi/AArQObkYN619mWbaC18SWSW+8IyCaWe2oSJHvNbuQCGGmEsv7Vb8MobuzE 2yfw== 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:from:dkim-signature; bh=6pmrSZyyR4jWZNcYhoy7izEaytdK1+RHhCYqNNK1RGo=; b=q0UW+3rVJGngJ/opQRkjqXzBgdxhQC3VZSbym4F5ZeWGW9Q/0xIGJV23DARg5wIR3/ Q2xs1KN4JZEjJMsExiOsmCg2bdyxHKIfSI+5fn86EQa1ikRjMHGrkPyj1MfRNUIFrjDP ucyQTIawhRPZG+IW4dyl+4XT1G6mrRETLntbfiStS3j0pe/HvhSZT3G7u+1Wk669/Po+ pFInGycx8VfqxE4yoX0quekd9e+DU4rDFXPhvuIpjm5FO6llkosu+qAWgJ/SkpyyJzoq /13RjOg6kH9KQvsCwSdwS02hqjKheKp7SdeJ/DrsXo6wG9FZHBB6XHh56z+cuDzUdfoO 33fA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=sSId7YSS; spf=pass (google.com: domain of steveawodey@gmail.com designates 2607:f8b0:4864:20::f32 as permitted sender) smtp.mailfrom=steveawodey@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-qv1-xf32.google.com (mail-qv1-xf32.google.com. [2607:f8b0:4864:20::f32]) by gmr-mx.google.com with ESMTPS id cp17-20020a056638481100b0040fc30ac205si185517jab.0.2023.05.05.04.06.10 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 05 May 2023 04:06:10 -0700 (PDT) Received-SPF: pass (google.com: domain of steveawodey@gmail.com designates 2607:f8b0:4864:20::f32 as permitted sender) client-ip=2607:f8b0:4864:20::f32; Received: by mail-qv1-xf32.google.com with SMTP id 6a1803df08f44-61b71b7803bso7784646d6.1; Fri, 05 May 2023 04:06:10 -0700 (PDT) X-Received: by 2002:a05:6214:1cc4:b0:5f1:89ba:c0dd with SMTP id g4-20020a0562141cc400b005f189bac0ddmr1051518qvd.30.1683284769054; Fri, 05 May 2023 04:06:09 -0700 (PDT) Received: from smtpclient.apple (pool-96-235-63-8.pitbpa.east.verizon.net. [96.235.63.8]) by smtp.gmail.com with ESMTPSA id z12-20020a0cf24c000000b0061b7bbb7624sm475853qvl.130.2023.05.05.04.06.08 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Fri, 05 May 2023 04:06:08 -0700 (PDT) From: Steve Awodey Content-Type: multipart/alternative; boundary="Apple-Mail=_FF0330DE-550D-422B-B73D-F56F6BB2B6DF" Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3731.500.231\)) Subject: [HoTT] Regensburg summer school Message-Id: <6F8CFB8C-D798-40A2-872A-D53A65AE4871@gmail.com> Date: Fri, 5 May 2023 07:05:57 -0400 Cc: CMUHoTT To: Homotopy Type Theory X-Mailer: Apple Mail (2.3731.500.231) X-Original-Sender: steveawodey@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=sSId7YSS; spf=pass (google.com: domain of steveawodey@gmail.com designates 2607:f8b0:4864:20::f32 as permitted sender) smtp.mailfrom=steveawodey@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: , --Apple-Mail=_FF0330DE-550D-422B-B73D-F56F6BB2B6DF Content-Type: text/plain; charset="UTF-8" Interactions of Proof Assistants and Mathematics, September 18-29, 2023, University of Regensburg. https://itp-school-2023.github.io/ The school will present state-of-the-art proof assistants from different angles: including theoretical foundations, engineering aspects, and applications in areas in mathematics and computer science. The goal of the summer school is to introduce proof assistants to students and researchers in both mathematics and computer science, while fostering collaboration and exchange between these communities. The programme will consist of short courses, research talks, tutorials, exercise sessions, and contributed talks. The list of speakers includes: Benedikt Ahrens Steve Awodey Andrej Bauer Yves Bertot Thierry Coquand John Harrison Angeliki Koutsoukou-Argyraki Conor McBride Paige Randall North Emily Riehl Michael Shulman Registration for participation and contributed talks will open in May and close on June 9. Updates and further information will be posted on the summer school homepage https://itp-school-2023.github.io/ . The summer school will take place in September 2023 in the town centre of Regensburg in Bavaria, Germany. The Old Town of Regensburg is listed as a UNESCO World Heritage Site, and considered the largest authentically preserved medieval city in Germany. -- 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/6F8CFB8C-D798-40A2-872A-D53A65AE4871%40gmail.com. --Apple-Mail=_FF0330DE-550D-422B-B73D-F56F6BB2B6DF Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset="UTF-8" Interactions of Proo= f Assistants and Mathematics,
September 18-29, 2023, University of Regensburg.
https://itp-schoo= l-2023.github.io/

The school will prese= nt state-of-the-art proof assistants from
different angles: including theoretical foundat= ions, engineering
aspects, and applications in areas in mathematics and computerscience. The goal of t= he summer school is to introduce proof
assistants to students and researchers in both mat= hematics and
c= omputer science, while fostering collaboration and exchange between<= br style=3D"caret-color: rgb(51, 51, 51); color: rgb(51, 51, 51); font-fami= ly: "Source Sans 3", sans-serif;">these communities. Th= e programme will consist of short courses,
research talks, tutorials, exercise sessions, = and contributed talks.

The list of speakers includes:
Benedikt Ahrens
Steve Awodey
Andrej Bauer
Yves Bertot
Thierry Coquand
John Harrison
Angeliki Koutsoukou-Argyraki
Conor McBride
Paige Randall North
Emily Riehl
Michael Shulman
<= div>
Registration for participation= and contributed talks will open in May
and close on June 9. Updates and further informat= ion will be posted on
the summer school homepage

--
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/msg= id/HomotopyTypeTheory/6F8CFB8C-D798-40A2-872A-D53A65AE4871%40gmail.com.=
--Apple-Mail=_FF0330DE-550D-422B-B73D-F56F6BB2B6DF--