From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9919 Path: news.gmane.org!.POSTED.blaine.gmane.org!not-for-mail From: nicolas tabareau Newsgroups: gmane.science.mathematics.categories Subject: EPIT 2020: Spring School on Homotopy Type Theory (first announcement) Date: Tue, 28 May 2019 10:13:32 +0200 Message-ID: Reply-To: nicolas tabareau Mime-Version: 1.0 (Mac OS X Mail 12.4 \(3445.104.11\)) Content-Type: text/plain; charset="utf-8" Content-Transfer-Encoding: quoted-printable Injection-Info: blaine.gmane.org; posting-host="blaine.gmane.org:195.159.176.226"; logging-data="132798"; mail-complaints-to="usenet@blaine.gmane.org" To: Original-X-From: majordomo@mlist.mta.ca Wed May 29 15:32:11 2019 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp2.mta.ca ([198.164.44.55]) by blaine.gmane.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.89) (envelope-from ) id 1hVygc-000YLu-M7 for gsmc-categories@m.gmane.org; Wed, 29 May 2019 15:32:10 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:50922) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1hVyh8-0004xE-6w; Wed, 29 May 2019 10:32:42 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1hVyec-0001Hh-0x for categories-list@mlist.mta.ca; Wed, 29 May 2019 10:30:06 -0300 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:9919 Archived-At: (This is the first announcement, details about the registration and = application procedure=20 will given in a second announcement after summer) =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. 25th-29th May 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 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 2019 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. -------------------------------------------------------------------- Lecturers Andrej Bauer (Ljubljana University):=20 Introduction to Homotopy Type Theory Bas Spitters (Aarhus University):=20 The Coq-HoTT library Andy Pitts (Cambridge 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 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]