From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10231 Path: news.gmane.io!.POSTED.ciao.gmane.io!not-for-mail From: nicolas tabareau Newsgroups: gmane.science.mathematics.categories Subject: EPIT 2020: Spring School on Homotopy Type Theory (new dates) Date: Fri, 5 Jun 2020 11:11:19 +0200 Message-ID: Reply-To: nicolas tabareau Mime-Version: 1.0 (Mac OS X Mail 13.4 \(3608.80.23.2.2\)) Content-Type: text/plain; charset="utf-8" Content-Transfer-Encoding: quoted-printable Injection-Info: ciao.gmane.io; posting-host="ciao.gmane.io:159.69.161.202"; logging-data="9722"; mail-complaints-to="usenet@ciao.gmane.io" To: Original-X-From: majordomo@rr.mta.ca Sun Jun 07 15:31:51 2020 Return-path: Envelope-to: gsmc-categories@m.gmane-mx.org Original-Received: from smtp2.mta.ca ([198.164.44.55]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1jhvOw-0002Nr-Vf for gsmc-categories@m.gmane-mx.org; Sun, 07 Jun 2020 15:31:51 +0200 Original-Received: from rr.mta.ca ([198.164.44.159]:55832) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1jhvOM-0005l1-6Y; Sun, 07 Jun 2020 10:31:14 -0300 Original-Received: from majordomo by rr.mta.ca with local (Exim 4.92.1) (envelope-from ) id 1jhvOA-00013Q-Mj for categories-list@rr.mta.ca; Sun, 07 Jun 2020 10:31:02 -0300 Precedence: bulk Xref: news.gmane.io gmane.science.mathematics.categories:10231 Archived-At: Important: Due to the sanitary crisis in May, the EPIT2020 summer school = has been postponed to October=20 =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D Spring School on Theoretical Computer Science (EPIT) =E2=80=93 Homotopy = Type Theory Ile d=E2=80=99Ol=C3=A9ron, CAES CNRS La vieille Perrotine, France. 19th-23th Oct 2020 https://epit2020cnrs.inria.fr =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D The EPIT is a French thematic school proposing, on an yearly basis, an = intensive 5-day long training,=20 specializing on a particular topic in theoretical computer science. It = is primarily addressed to PhD students,=20 Post-doctoral researchers and junior academics. The 2020 edition of the EPIT will be centered around Homotopy Type = Theory, a research topic at the junction=20 of Computer Science and Mathematics. Our hope is hence to provide an = introduction that is accessible=20 to researchers in both areas. Pre-registration is now open, please visit = https://epit2020cnrs.inria.fr/registration/ = to know more.=20 For any question, please contact epit2020@sciencesconf.org = If you already know that you can not attend, but wish to follow live = streams of the talks, please=20 send a mail to epit2020@sciencesconf.org = so that we can plan the right tool. NB: As the number of places is limited, we have fixed a deadline for = pre-registration to ** March 15, 2020 **. -------------------------------------------------------------------- Lecturers Andrej Bauer (Ljubljana University):=20 Introduction to Homotopy Type Theory Bas Spitters (Aarhus University):=20 The Coq-HoTT library Egbert Rijke (Ljubljana University):=20 Models of (Univalent) Type Theory Anders Mo=CC=88rtberg (Stockholm University):=20 Cubical Type Theory Guillaume Brunerie (Stockholm University):=20 Synthetic Homotopy Theory -------------------------------------------------------------------- Talks Paige North (Ohio State University):=20 Directed Homotopy Type Theory Valery Isaev (JetBrain, Saint Petersburg):=20 The Arend proof assistant [For admin and other information see: http://www.mta.ca/~cat-dist/ ]