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.6 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, 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-x238.google.com (mail-oi1-x238.google.com [2607:f8b0:4864:20::238]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id bae3fa1d for ; Fri, 28 Feb 2020 12:32:32 +0000 (UTC) Received: by mail-oi1-x238.google.com with SMTP id x207sf1032057oix.19 for ; Fri, 28 Feb 2020 04:32:32 -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=MMsqABMFFV3AOELzRgxm8nFojBChmOsPkxAm4OG12VA=; b=LXlLW+JVc7YnY7InVdsmckyBK8a4WKLV2g52CqjaKFB4koKeW2MmekW+nfPA+DisqH 2dKOaKFvZSM/qZL+OXd9aPTm3DvIXiokccXFgsXb/q9/rSBiNSz4vwFHwXVdBoLeN8tR hLkRoDbOzxUE+iNbeHICOGViOBcXltiEYyYzgeidi0dODWMnEQu43i6vTd+BmNMaFIiC BnI4lfohLzDQPd1I2cbRAL6gf1VUhAjxHT18KTTDZxgXJ8yoJG6l4QvXGNerT5Oh2I2Z V3OhU+REBA0Ze4ER1RrrKODUEwBu/YRQfOLEGtpBbw6p1N5DZJzmuZ6ROkst0IZ2+tHQ u/Gg== 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=MMsqABMFFV3AOELzRgxm8nFojBChmOsPkxAm4OG12VA=; b=ZUUGAMvWzprBOUMHWm2RtB8uHY/mNxCKlwHV0zf+SMlCO3zUe8EXaWwRlRY6OO/Ls8 mRdI2RNBgGyzX+LebtgBFqyMKRiBghCwV3d1cv06SNGE6k6PUl6yrX+zgbmSvex+qTmd k4vG/cVpyYBfNkdhzRZeMK+b/lRc+iY224lY+GEqOY9sCvToHlMGOvsOXobTsH+ohm78 7UZsdciQgSCJWxd7tXRINheOlG4Q7RkcraepxNSe27u5kXIutKWU/ONOe60upXV31c2w oydDjR/3KUm1MXIEPmYcJ5bY+2sb03Vhd0Ie1cIlprqkz5l78A5UFUBPf9T0cDbxMCh7 ZoaA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUQVZ/GI61DYTsc332eqbR2hQ0BKEaxQNSAkCrAgsLonhoCZ2Vh fE19dBPDJ3dzX3EzlyGsXVo= X-Google-Smtp-Source: APXvYqyvsMTERjqtEAWiWX2UDA9TuG7kpDbFNYfYA63dIBYCh0oMX39w+jdmZevlc/sgvQcIwE2ixA== X-Received: by 2002:a9d:7509:: with SMTP id r9mr2995287otk.270.1582893150615; Fri, 28 Feb 2020 04:32:30 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:4a96:: with SMTP id i22ls963432otf.9.gmail; Fri, 28 Feb 2020 04:32:30 -0800 (PST) X-Received: by 2002:a05:6830:18d4:: with SMTP id v20mr3141274ote.29.1582893149849; Fri, 28 Feb 2020 04:32:29 -0800 (PST) Date: Fri, 28 Feb 2020 04:32:29 -0800 (PST) From: Chuangjie Xu To: Homotopy Type Theory Message-Id: Subject: [HoTT] 5th autumn school "Proof and Computation" MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_249_1038967041.1582893149149" X-Original-Sender: xcjstyle@msn.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_249_1038967041.1582893149149 Content-Type: multipart/alternative; boundary="----=_Part_250_1290334521.1582893149149" ------=_Part_250_1290334521.1582893149149 Content-Type: text/plain; charset="UTF-8" [Apologies for multiple postings.] Autumn school "Proof and Computation" Fischbachau, Germany, 20th to 26th September 2020 http://www.mathematik.uni-muenchen.de/~schwicht/pc20.php The fifth international autumn school "Proof and Computation" will be held from 20th to 26th September 2020 in Fischbachau near Munich. Its aim is to bring together young researchers in the field of Foundations of Mathematics, Computer Science and Philosophy. SCOPE -------------------- - Predicative Foundations - Constructive Mathematics and Type Theory - Computation in Higher Types - Extraction of Programs from Proofs COURSES -------------------- - Steve Awodey: Categorical logic - Marc Bezem: Coherent logic - Hajime Ishihara: Reverse mathematics in constructive set theory - Stefan Neuwirth: The philosophy of dynamic algebra - Frederik Nordvall Forsberg: Universes of data types in constructive type theory - Monika Seisenberger: Extraction of programs from proofs - Chuangjie Xu: Various approaches to compute moduli of continuity WORKING GROUPS -------------------- There will be an opportunity to form ad-hoc groups working on specific projects, but also to discuss in more general terms the vision of constructing correct programs from proofs. APPLICATIONS -------------------- Graduate or PhD students and young postdoctoral researches are invited to apply. Applications (e.g. a self-introduction including research interests and motivation) should be sent to Chuangjie Xu . Students are required to provide also a letter of recommendation, preferably from the thesis adviser. Deadline for applications: **30 May 2020**. Applicants will be notified by 20th June 2020. FINANCIAL SUPPORT -------------------- Successful applicants will be offered **full-board accommodation** for the days of the autumn school. There are NO funds, however, to reimburse travel or further expenses, which successful applicants will have to cover otherwise. The workshop is supported by the Udo Keller Stiftung (Hamburg), the CID (Computing with Infinite Data) programme of the European Commission and a JSPS core-to-core project. Klaus Mainzer Peter Schuster Helmut Schwichtenberg -- 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/d459f9a3-0791-4b32-9e17-7fcba5aa0ccb%40googlegroups.com. ------=_Part_250_1290334521.1582893149149 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
[Apo= logies for multiple postings.]

= =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Autumn school "Proof and Com= putation"
=C2=A0 = =C2=A0 =C2=A0 =C2=A0 Fischbachau, Germany, 20th to 26th September 2020
=C2=A0 =C2=A0=C2=A0http://www.= mathematik.uni-muenchen.de/~schwicht/pc20.php

The fifth international autumn school "Proof and Computation= " will be held
from= 20th to 26th September 2020 in Fischbachau near Munich.=C2=A0 Its aim is t= o
<= span style=3D"color: rgb(0, 0, 0); font-family: "Lucida Console",= Courier, "Courier New"; font-size: 12px;">bring together young r= esearchers in the field of Foundations of Mathematics,
Computer Science and Philosophy.

SCOPE
--------------------
- Predicative Foundations
- Constructive Mathematics and Type Theory
- Computation in Higher Types
- Extraction of Programs from Proofs

COURSES
--------------------
- Steve Awodey: Categorical logic
- Marc Bezem: Coherent logic
- Hajime Ishihara: Reverse mathe= matics in constructive set theory
- Stefan Neuwirth: The philosophy of dynamic algebra
- Frederik Nordvall Forsberg: Univer= ses of data types in constructive type theory
- Monika Seisenberger: Extraction of programs from pr= oofs
- Chuangjie Xu: Var= ious approaches to compute moduli of continuity

WORKING GROUPS
--------------------
There will be an opportunity to form ad-hoc groups working on specific
projects, but also to dis= cuss in more general terms the vision of
constructing correct programs from proofs.

APPLICATIONS
--------------------
Graduate or PhD students and young postdoctoral researches are= invited to
apply.=C2=A0= Applications (e.g. a self-introduction including research interests=
and motivation) should be sent= to

=C2=A0 Chuangjie Xu <xu@ma= th.lmu.de>.

Students are requi= red to provide also a letter of recommendation, preferably
from the thesis adviser.

Deadline for applications: **30 May 2020**.
Applicants will be notified= by 20th June 2020.

FINANCIAL SUP= PORT
-------------------= -
<= span style=3D"color: rgb(0, 0, 0); font-family: "Lucida Console",= Courier, "Courier New"; font-size: 12px;">Successful applicants = will be offered **full-board accommodation** for
the days of the autumn school.=C2=A0 There are NO = funds, however, to reimburse
travel or further expenses, which successful applicants will have to
cover otherwise.
The workshop is supported by the Udo Ke= ller Stiftung (Hamburg), the
CID (Computing with Infinite Data) programme of the European Commissio= n
<= span style=3D"color: rgb(0, 0, 0); font-family: "Lucida Console",= Courier, "Courier New"; font-size: 12px;">and a JSPS core-to-cor= e project.

<= br style=3D"padding: 0px; color: rgb(0, 0, 0); font-family: "Lucida Co= nsole", Courier, "Courier New"; font-size: 12px;">Klaus Mainzer
Peter Schuster
Helmut Schwichtenberg

--
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/d459f9a3-0791-4b32-9e17-7fcba5aa0ccb%40googleg= roups.com.
------=_Part_250_1290334521.1582893149149-- ------=_Part_249_1038967041.1582893149149--