From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9918 Path: news.gmane.org!.POSTED.blaine.gmane.org!not-for-mail From: nicolas tabareau Newsgroups: gmane.science.mathematics.logic.coq.club,gmane.science.mathematics.categories,gmane.comp.lang.agda,gmane.comp.science.types.announce Subject: EPIT 2020: Spring School on Homotopy Type Theory (first announcement) Date: Tue, 28 May 2019 10:13:32 +0200 Message-ID: <27D35CDE-A044-4C13-88A4-BD3A025A05B8@inria.fr> Reply-To: coq-club@inria.fr Mime-Version: 1.0 (Mac OS X Mail 12.4 \(3445.104.11\)) Content-Type: multipart/alternative; boundary="Apple-Mail=_ED9A7CEC-D5AC-4D0E-A212-B7A6BECB8B90" Injection-Info: blaine.gmane.org; posting-host="blaine.gmane.org:195.159.176.226"; logging-data="243480"; mail-complaints-to="usenet@blaine.gmane.org" Cc: Matthieu Sozeau To: categories@mta.ca, coq-club@inria.fr, agda@lists.chalmers.se, types-announce@lists.seas.upenn.edu, EUTypes mailing list Original-X-From: coq-club-owner@inria.fr Tue May 28 10:13:42 2019 Return-path: Envelope-to: gsmlcc-coq-club@gmane.org Original-Received: from mail2-relais-roc.national.inria.fr ([192.134.164.83]) by blaine.gmane.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.89) (envelope-from ) id 1hVXEr-0011Bn-BO for gsmlcc-coq-club@gmane.org; Tue, 28 May 2019 10:13:41 +0200 X-IronPort-AV: E=Sophos;i="5.60,521,1549926000"; d="scan'208,217";a="384992786" Original-Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 28 May 2019 10:13:39 +0200 Original-Received: by sympa.inria.fr (Postfix, from userid 20132) id D8E177ED69; Tue, 28 May 2019 10:13:39 +0200 (CEST) Original-Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 55A377ED69 for ; Tue, 28 May 2019 10:13:33 +0200 (CEST) X-IronPort-AV: E=Sophos;i="5.60,521,1549926000"; d="scan'208,217";a="384992753" Original-Received: from nat5.emn.fr (HELO dhcp-10-44-192-150.emn.fr) ([193.54.76.165]) by mail2-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 28 May 2019 10:13:32 +0200 X-Mailer: Apple Mail (2.3445.104.11) X-Loop: coq-club@inria.fr X-Sequence: 17693 Errors-to: coq-club-owner@inria.fr Precedence: list Precedence: bulk Original-Sender: coq-club-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: X-Gmane-Expiry: 2019-06-11 Xref: news.gmane.org gmane.science.mathematics.logic.coq.club:22205 gmane.science.mathematics.categories:9918 gmane.comp.lang.agda:11108 gmane.comp.science.types.announce:8446 Archived-At: --Apple-Mail=_ED9A7CEC-D5AC-4D0E-A212-B7A6BECB8B90 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 (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 --Apple-Mail=_ED9A7CEC-D5AC-4D0E-A212-B7A6BECB8B90 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
(This is the = first announcement, details about the registration and = application procedure 
 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<= /font>

Spring = School on Theoretical Computer Science (EPIT) =E2=80=93 Homotopy Type = Theory

Ile d=E2=80=99Ol=C3=A9ro= n, 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, 
specializing on a particular topic in = theoretical computer science. It is primarily addressed to = PhD students, 
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 
of Computer Science and Mathematics. Our = hope is hence to provide an introduction that = is accessible 
to researchers in both areas.


---------------------------------------------------------------= -----
Lecturers

Andrej Bauer (Ljubljana = University): 
Introduction to Homotopy Type Theory

Bas Spitters (Aarhus = University): 
The Coq-HoTT library

Andy Pitts (Cambridge = University): 
Models of (Univalent) Type Theory

Anders Mo=CC=88rtberg (Stockholm = University): 
Cubical Type Theory

Guillaume Brunerie (Stockholm = University): 
Synthetic Homotopy Theory




= --Apple-Mail=_ED9A7CEC-D5AC-4D0E-A212-B7A6BECB8B90--