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.9 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-x23d.google.com (mail-oi1-x23d.google.com [2607:f8b0:4864:20::23d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 35edc3e4 for ; Mon, 2 Mar 2020 19:14:50 +0000 (UTC) Received: by mail-oi1-x23d.google.com with SMTP id n4sf447154oih.12 for ; Mon, 02 Mar 2020 11:14:50 -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=hL/Jz9OKSaDJ+gvKLuZDtMym6tp0w34fETnDVmuENn8=; b=ssCb16LyLHRZrUqIhOns9AqzbtwnttzcMvMQIXgZb7z2aH5dUzFkohwuhBuGGhHrnV OBgJX3GN7M6SHsKPyERRgnkpCVUxBJsQvvBi/KvE6sX3ttPntWjVGeAmKQeXAEFLG3dS ogDgVe7q5veXNOa9dw7AjTe65MOJaJNvhlUbxDuo/PVtDgmQQupV+q8ugGn8k2EpG8z4 CnMkrbi3xB95lR7+g4OUoqRHY9mDHHbb4jP4VHTG8+yQAoaaANwYF4igfM4FjOYQYDb2 xJk0HUC20dVWL5/qBEV8wwZ9h6C/gy8Wz5JLjCdyM1hEaDa84scu2e1XztQn5Y1OWmvG l6SA== 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=hL/Jz9OKSaDJ+gvKLuZDtMym6tp0w34fETnDVmuENn8=; b=l2pD13v/E1Ts3dXyiZR8GaBFszke3cQgpu6RfnWlaUHmSpALoLumJLrjtMFP9nac5R xQLuVFrlRdzWudHrwZfZepKcAsq6d5d4awHs0AM48OZnREkxuwacbXwsupwH0a/BbD44 T33Y/p7J4rBIjKdN1TU7+xlf0PrKUbPbqBYrLMer1UZrHIgW7egg8bIlL/vxpWZpcJR0 EgXxYyVXZw6hMmtEgoJGtS/NSjCg9F0hvUW2Y1t1eM0k60PjAYqH4ipJLR+k23jUyc8X zoWpcqYOT10T6Mp/fDJe9jM0hiQwIGXVUeQ3GnHu+J7pNjkv9LafQcDJf3R3UpqMzsOd fZGA== 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=hL/Jz9OKSaDJ+gvKLuZDtMym6tp0w34fETnDVmuENn8=; b=ApCF0shKM3i26RzZzixmPWv9u+U6WhhwE5IRDC/TqpXtdVd3I/pnSeRbsMXKNFj3Dx jOltIrunqi69V3gM9eng+Tcyhpe7H04JcPYEirFA7PVLWjpuonSt46gqmzqQVClaXUBk PTc/c4NQVvxKU2R8ehceUVtnMfxImiYntweR83uGt+baLJLB2C9P7fgYNJiDSe5ZWXIY Fjw7xA961PJ6fZ5mXQKnF/TzqG3QDXzpHLjCKyUNEgMm94UsF0EvuF5bNVnokjg28j1N 1Bg1h5z/H2eH+smdUxXoEwhs/RyY3WlR4YmcSHKaZA3V/MZF+PGCIw48GbRkynTiYiZz xj8g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANhLgQ3RSVAEOvKsbknDs6tQuAztaavQPx6yZ9porJmvSNG41rswYyDn CVjcAjQMzyvgG+39L0lzFTA= X-Google-Smtp-Source: ADFU+vudeIu9kowTfOxTRnNvG3oGzUOU55mHfEfGVVLnj+5g03aS8N80Itcec+5HS0XKv0pZb4zsBg== X-Received: by 2002:a05:6830:1c8:: with SMTP id r8mr531177ota.63.1583176489023; Mon, 02 Mar 2020 11:14:49 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:7999:: with SMTP id h25ls168088otm.2.gmail; Mon, 02 Mar 2020 11:14:48 -0800 (PST) X-Received: by 2002:a9d:20c1:: with SMTP id x59mr553601ota.286.1583176488463; Mon, 02 Mar 2020 11:14:48 -0800 (PST) Date: Mon, 2 Mar 2020 11:14:47 -0800 (PST) From: nicolas tabareau To: Homotopy Type Theory Message-Id: <0e10d866-00f3-4311-90a9-f704ef26e10b@googlegroups.com> Subject: [HoTT] EPIT 2020: Spring School on Homotopy Type Theory (last announcement) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1222_81222962.1583176487959" 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_1222_81222962.1583176487959 Content-Type: multipart/alternative; boundary="----=_Part_1223_701438149.1583176487960" ------=_Part_1223_701438149.1583176487960 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable [This is a reminder that the deadline for pre-registration is ** March 15,= =20 2020 **, note=20 that we are pleased to have to new lectures by Valery Isaev and Paige=20 North] =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=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 Guillaume Brunerie (Stockholm University):=20 Synthetic Homotopy Theory Valery Isaev (JetBrain, Saint Petersburg):=20 The Arend proof assistant Anders Mo=CC=88rtberg (Stockholm University):=20 Cubical Type Theory Paige North (Ohio State University):=20 Directed Homotopy Type Theory Andy Pitts (Cambridge University):=20 Models of (Univalent) Type Theory Bas Spitters (Aarhus University):=20 The Coq-HoTT library --=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/0e10d866-00f3-4311-90a9-f704ef26e10b%40googlegroups.com. ------=_Part_1223_701438149.1583176487960 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
[This is a reminder that the deadline for pre-registratio= n is ** March 15, 2020 **, note=C2=A0
=C2=A0that we are pleased to ha= ve to new lectures by Valery Isaev and Paige North]

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=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 Com= puter Science (EPIT) =E2=80=93 Homotopy Type Theory

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

25th-29th Ma= y 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=C2=A0EPIT=C2=A0is a French thematic= school proposing, on an yearly basis, an intensive 5-day long training,=C2= =A0
specializing on a parti= cular topic in theoretical computer science. It is primarily addressed to P= hD=C2=A0students,=C2=A0
Pos= t-doctoral researchers and junior academics.

T= he 2020 edition of the EPIT will be centered around Homotopy Type Theory, a= research topic at the=C2=A0junction=C2=A0
of Computer Science and Mathematics. Our hope is hence to p= rovide an introduction that is=C2=A0accessible=C2=A0
to researchers in both areas.
Pre-registration is now open, please visit=C2=A0https://epit2020cnrs.in= ria.fr/registration/=C2=A0to know more.=C2=A0

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

NB: As the number of places is limited, we have fi= xed a deadline for pre-registration to ** March 15, 2020 **.
<= br class=3D"">
-------------------= -------------------------------------------------
Lecturers

Andrej Bauer=C2=A0(Ljubljana Univers= ity):=C2=A0
Introduction to= Homotopy Type Theory

Guillaume = Brunerie=C2=A0(Stockholm University):=C2=A0
Synthetic Homotopy Theory

Vale= ry Isaev=C2=A0(JetBrain, Saint Petersburg):=C2=A0
The Arend proof assistant

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

Paige = North=C2=A0(Ohio State University):=C2=A0
Directed Homotopy Type Theory

Andy P= itts=C2=A0(Cambridge University):=C2=A0
Models of (Univalent) Type Theory<= /font>
<= div dir=3D"ltr" class=3D"">Bas Spitters=C2=A0(Aarhus University):=C2=A0
The Coq-Ho= TT library

--
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/0e10d866-00f3-4311-90a9-f704ef26e10b%40googleg= roups.com.
------=_Part_1223_701438149.1583176487960-- ------=_Part_1222_81222962.1583176487959--