From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.7 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-oi1-x240.google.com (mail-oi1-x240.google.com [2607:f8b0:4864:20::240]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 52bad1b1 for ; Thu, 30 Jan 2020 13:05:55 +0000 (UTC) Received: by mail-oi1-x240.google.com with SMTP id j142sf1399343oib.23 for ; Thu, 30 Jan 2020 05:05:55 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=Zvf2ttvO35g7aawpZxUOEVzwyNFEaAU6ozFibdN5j0s=; b=ESPoE7HC1FfqiQ1Q1TF5XgGitfPMXAErNDYa+47K/2eu8S611KvEKLEuATPIti7g9G B4FgxjUSQIUPa26n5tSO6eoDVEaqEGEGXHRQMDj5/zwWnZde5rIiObhktGkTbJ12KQpI hiUc5u6vD3YdXYrznkev4PnX1ohG5vHm+7ytkwRjF9V135tZguEi7Il84TkTlBEz0I7t c/FRsCkD0rVNiXB8qBEhuaWON6sFcO+GdG2D8IHUUrt6nsGI9vhA1azT5JShX3UdO1G0 7teKSm7v97OymI9tCauuBks22TrhoPeW7B7oJ5jEsv3gVpJyOz/by794v5RnMYjSkIeg sR6w== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=Zvf2ttvO35g7aawpZxUOEVzwyNFEaAU6ozFibdN5j0s=; b=Fl1K7BinBVGvXBtK1eZKu1EQujBhNgXkYRatbe7tFM2Z+h0EmY5ZyMmq4URzk4Sne4 Vpl30O4vxOcCe2TJSvp2GzQVQ/TCRzBuVvayOQr0gM/94Ho7lCntEwcYkdVUdUuUnjO0 7w6VolOXhwmh4YHN3Sj8YMj9KA6ke2d70ogglBsf9ecEE0/rKn8Ch/kDXMWSF6b66rDs g6zB3HtqnFvaPBwQh+zkfCo9fvtC3aLPYoqKbtceaeXEgPu0TaqIO9QV9pLtxl2Ue2rE pMnSlQhw2HfIFRhM/vS7nn8e2VGspLPykK9QuJsdYm3+nipPmy4hpIqGjBYaVy6TIy0u ZphQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=Zvf2ttvO35g7aawpZxUOEVzwyNFEaAU6ozFibdN5j0s=; b=tWoDCGS71CXrdRbwRz/L+QJWU21jmtmFUEn4yNfErlrrB/fIRQCdx4n+OS1BYvKYpU 3Zh6IMw9fiGUEBGXoKQCZOd66+q6flI7E/rwoe8zwSJC8heGvejw/1znZz+cSLErh85K DR3I7LVBuVTs8T1f8CXeRdSam6ZZoFya5sXloyc7mxHCh6jiQ5CuUTovK3+csBa1mIZ9 jN6c5My29e/Zmky4N57vesSxYBr6nLMcsmMe6rc1GD4+YefCKveGm9F60CJNpV9jpAPH lSXQRbXWxh/z/R800RjBU1T0+pRWtdypmOLWzxwAVk0wi/WKqHVh9v4S+zPa0kz8gyoa KW5w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXMQXk/eY8tlXDud+rNptQbOHA6bIgrNHv8nvTFefYNkWy3G6yd QvJrQK4QxUZEAXDe2pj/fHQ= X-Google-Smtp-Source: APXvYqxbfq86whXActILuqAh0f/wCj5H06CANOIxy1MUN8VQtMF0mg6MZUtzaUCCHGK484TGtHz0Gw== X-Received: by 2002:a9d:74c4:: with SMTP id a4mr3490430otl.119.1580389553564; Thu, 30 Jan 2020 05:05:53 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6808:a0a:: with SMTP id n10ls719697oij.0.gmail; Thu, 30 Jan 2020 05:05:53 -0800 (PST) X-Received: by 2002:a05:6808:4c2:: with SMTP id a2mr2649064oie.118.1580389552841; Thu, 30 Jan 2020 05:05:52 -0800 (PST) Date: Thu, 30 Jan 2020 05:05:52 -0800 (PST) From: nicolas tabareau To: Homotopy Type Theory Message-Id: <221d36fb-a065-404f-9664-e474734713a6@googlegroups.com> Subject: [HoTT] EPIT 2020: Spring School on Homotopy Type Theory (second announcement) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1470_1158227582.1580389552208" X-Original-Sender: tabareau.nicolas@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: , ------=_Part_1470_1158227582.1580389552208 Content-Type: multipart/alternative; boundary="----=_Part_1471_90622591.1580389552208" ------=_Part_1471_90622591.1580389552208 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=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 Typ= e 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=3D The EPIT is a French thematic school proposing, on an yearly basis, an=20 intensive 5-day long training,=20 specializing on a particular topic in theoretical computer science. It is= =20 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,= =20 a research topic at the junction=20 of Computer Science and Mathematics. Our hope is hence to provide an=20 introduction that is accessible=20 to researchers in both areas. Pre-registration is now open, please visit=20 https://epit2020cnrs.inria.fr/registration/ to know more.=20 For any question, please contact epit2020@sciencesconf.org NB: As the number of places is limited, we have fixed a deadline for=20 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 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 --=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/221d36fb-a065-404f-9664-e474734713a6%40googlegroups.com. ------=_Part_1471_90622591.1580389552208 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =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 Theo= retical Computer Science (EPIT) =E2=80=93 Homotopy Type Theory

Ile d=E2=80=99Ol=C3=A9ron, CAES CNRS=C2=A0La vieill= e Perrotine, France.

25th-29th May 2020

=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=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=C2=A0EPIT=C2=A0is a Fre= nch thematic school proposing, on an yearly basis, an intensive 5-day long = training,=C2=A0
specializin= g on a particular topic in theoretical computer science. It is primarily ad= dressed to PhD=C2=A0students,=C2=A0
Post-doctoral researchers and junior academics.

The 2020 edition of the EPIT will be centered around Homotopy Ty= pe Theory, a research topic at the=C2=A0junction=C2=A0
of Computer Science and Mathematics. Our hope i= s hence to provide an introduction that is=C2=A0accessible=C2=A0
to researchers in both areas.

Pre-registration is now open, please visit=C2=A0https://epit2= 020cnrs.inria.fr/registration/=C2=A0to know more.=C2=A0

For any question, please contact=C2=A0epit2020@sciencesconf.org

<= div dir=3D"ltr" class=3D"" style=3D"font-family: Helvetica; font-size: 12px= ; text-size-adjust: auto; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">= NB: As the number of places is limited, = we have fixed a deadline for pre-registration to ** March 15, 2020 **.

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

Andrej Bauer=C2=A0(Ljubljana= University):=C2=A0
Introdu= ction to Homotopy Type Theory

Bas Spitters=C2=A0(Aarhus University):=C2= =A0
The Coq-HoTT library
Andy Pitts=C2=A0(Cambridge University):=C2=A0
Models of (Univalent) Type Theory
Anders Mo=CC= =88rtberg=C2=A0(Stockholm University):=C2=A0
Cubical Type Theory

<= /div>
Guillaume Brunerie=C2=A0(Stockholm= University):=C2=A0
Synthet= ic Homotopy Theory

--
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.co= m/d/msgid/HomotopyTypeTheory/221d36fb-a065-404f-9664-e474734713a6%40googleg= roups.com.
------=_Part_1471_90622591.1580389552208-- ------=_Part_1470_1158227582.1580389552208--