From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 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,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: from mail-yw1-x1139.google.com (mail-yw1-x1139.google.com [IPv6:2607:f8b0:4864:20::1139]) by inbox.vuxu.org (Postfix) with ESMTP id 82E0E23228 for ; Tue, 12 Mar 2024 06:11:21 +0100 (CET) Received: by mail-yw1-x1139.google.com with SMTP id 00721157ae682-607838c0800sf66642017b3.1 for ; Mon, 11 Mar 2024 22:11:21 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20230601; t=1710220281; x=1710825081; darn=inbox.vuxu.org; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:x-original-sender:mime-version:subject :message-id:to:from:date:sender:from:to:cc:subject:date:message-id :reply-to; bh=p1NZ18kfrLPFPy3diMKRmSpDO9qEfWT4Rh2z3oWZCPc=; b=JHy7vQyQHEaccwAwHq5yj4dAVD2b9Cvep5wm9e14wvXf10T65An3UVbGU78Dzft83c ovI1xa8aL00scKqiG8tcZaJS6cXJp/LQzvoCk0OayZvPb1CmroZgSF3owQeBEysNkW/v aA3WPjX8SxJvzREhnBshf/ByM7zwOvJgHsP4US3ebuK67yjLWpJaPKQQzpIG2+X++39M TZI+g14U+QUGd3fynPTbAAXJbua+jVWP11nCkjfhHfTJFGYdK91aHfXVaEP1SRLXWxrw LtMSS7nNvGNi+TNMHohlRla6zRNX5M6Q47Dbv23J0YeYNQrZTByx0Jq+8TLRfrsUrhIG Kapg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1710220281; x=1710825081; h=list-unsubscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-sender:mime-version:subject:message-id:to:from:date :x-beenthere:x-gm-message-state:sender:from:to:cc:subject:date :message-id:reply-to; bh=p1NZ18kfrLPFPy3diMKRmSpDO9qEfWT4Rh2z3oWZCPc=; b=UHYDdrjX3cfrwNb2iab7tPlrjP1pCMi+/sAfq0oX32vQ2xdHtOWwkuAu4sjbP53dnD ANmS3+GBmQ/aJ6PmKJOyxXmbKBiXuAbqg9L0NHRel4gxzGP6mTZDZn4BbFHE12PvbwkU vhXqkN5V7kzZfW/z36G5PkYSp5S1BL23J4VOjcE7cu4fhneyhGGhWfaUtlxwbdyiQSQ8 6kYnfdpHqPAkqAQVUuybGSZqSdtgNENRpwKhBtDXVlDrrBuWv0/vupC2LI3/M8BPALCA hmpbUq0/HRZLitvQ1cIa3A79jkK4pPUJP/PI8TZ2uWZYkXo/li6ab1iQdM9AWyfdwTLf 8epw== Sender: homotopytypetheory@googlegroups.com X-Forwarded-Encrypted: i=1; AJvYcCWtCppeyK8JlWptyrfUyL2sf4qeOY18N8ABtiUrStWNNwlqAd7hyw9phlAo0r5j6ZldRFHo0AfLyDRBHHVNrbDmSw== X-Gm-Message-State: AOJu0YznccWbbZ15qnP0XAxiTjlcvOuUnHWZvbbK4tqmkpuMOFi4qplF t8Fw9/FQyAjecWmfe/Ci/FAe2KxSVg7P66g6Qn8XcNvNBuMx8gdC X-Google-Smtp-Source: AGHT+IG1R1+n2UtoOoqc0phMvbYFGSLvyumd0RFZZcedwl8Z+o3RkFz4n25CO6w4ntXVZ+yVwIVw7A== X-Received: by 2002:a25:5384:0:b0:dc2:201a:7f1a with SMTP id h126-20020a255384000000b00dc2201a7f1amr5733209ybb.30.1710220280736; Mon, 11 Mar 2024 22:11:20 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:ab2b:0:b0:dcc:be89:34e3 with SMTP id u40-20020a25ab2b000000b00dccbe8934e3ls3675621ybi.1.-pod-prod-05-us; Mon, 11 Mar 2024 22:11:18 -0700 (PDT) X-Received: by 2002:a25:68ca:0:b0:dc2:466a:23c4 with SMTP id d193-20020a2568ca000000b00dc2466a23c4mr2235779ybc.4.1710220278344; Mon, 11 Mar 2024 22:11:18 -0700 (PDT) Date: Mon, 11 Mar 2024 22:11:17 -0700 (PDT) From: Chuangjie Xu To: Homotopy Type Theory Message-Id: <1d998bbd-5158-4550-a1dc-4caaa6146062n@googlegroups.com> Subject: [HoTT] Autumn school "Proof and Computation", Fischbachau (Germany), 15-21 Sep 2024 MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_24144_1020696311.1710220277197" 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_24144_1020696311.1710220277197 Content-Type: multipart/alternative; boundary="----=_Part_24145_381520336.1710220277197" ------=_Part_24145_381520336.1710220277197 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable [Apologies for multiple postings.] Autumn school "Proof and Computation" Fischbachau, Germany, 15th to 21st September 2024 http://www.mathematik.uni-muenchen.de/~schwicht/pc24.php This year's international autumn school "Proof and Computation" will be hel= d from 15th to 21st September 2024 in Fischbachau near Munich. Its aim is to= =20 bring together young researchers in the field of Foundations of Mathematics,=20 Computer Science and Philosophy. SCOPE -------------------- - Predicative Foundations - Constructive Mathematics and Type Theory - Computation in Higher Types - Extraction of Programs from Proofs COURSES -------------------- - Thierry Coquand (Gothenburg): Topos theory and constructive mathematics - Klaus Mainzer (Munich): From Proof and Computation to AI - Logical,=20 Mathematical, and Philosophical Foundations - Gerhard J=C3=A4ger (Bern): Foundations of explicit mathematics - Sara Negri (Padua): Enriched syntax for enhanced proof theory - Monika Seisenberger (Swansea): Extraction of programs from proofs - Holger Thies (Kyoto): Extracting efficient programs from proofs in=20 analysis - Freek Wiedijk (Nijmegen): The De Bruijn criterion versus the Poincare=20 principle 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 researchers 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, preferabl= y from the thesis adviser. Please specify in your application whether you are interested in applying= =20 for financial support (details provided below). Deadline for applications: **7th June 2024**. Applicants will be notified by 24th June 2024. FINANCIAL SUPPORT -------------------- Successful applicants are eligible to apply for financial support that=20 covers accommodation and meals for the duration of the autumn school (approximatel= y 116 Euros per day). Please note that there are no funds available for the reimbursement of travel or additional expenses, which successful applicants will need to cover independently. The workshop is supported by the Udo Keller Stiftung (Hamburg) and the COST Action EuroProofNet. Klaus Mainzer Peter Schuster Helmut Schwichtenberg --=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/1d998bbd-5158-4550-a1dc-4caaa6146062n%40googlegroups.com= . ------=_Part_24145_381520336.1710220277197 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable [Apologies for multiple postings.]

=C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0Autumn school "Proof and Computation"
=C2=A0 =C2=A0 Fischbachau,= Germany, 15th to 21st September 2024
=C2=A0http://www.mathematik.uni-= muenchen.de/~schwicht/pc24.php

This year's international autumn = school "Proof and Computation" will be held
from 15th to 21st Septembe= r 2024 in Fischbachau near Munich. Its aim is to bring
together young = researchers in the field of Foundations of Mathematics, Computer
Scien= ce and Philosophy.

SCOPE
--------------------
- Predic= ative Foundations
- Constructive Mathematics and Type Theory
- Co= mputation in Higher Types
- Extraction of Programs from Proofs
COURSES
--------------------
- Thierry Coquand (Gothenburg): = Topos theory and constructive mathematics
- Klaus Mainzer (Munich): Fr= om Proof and Computation to AI - Logical, Mathematical, and Philosophical F= oundations
- Gerhard J=C3=A4ger (Bern): Foundations of explicit mathem= atics
- Sara Negri (Padua): Enriched syntax for enhanced proof theory<= br />- Monika Seisenberger (Swansea): Extraction of programs from proofs- Holger Thies (Kyoto): Extracting efficient programs from proofs in ana= lysis
- Freek Wiedijk (Nijmegen): The De Bruijn criterion versus the P= oincare principle

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
con= structing correct programs from proofs.

APPLICATIONS
------= --------------
Graduate or PhD students and young postdoctoral researc= hers are invited to
apply. =C2=A0Applications (e.g. a self-introductio= n including research interests
and motivation) should be sent to
=
Chuangjie Xu <xu@math.lmu.de>.

Students are required= to provide also a letter of recommendation, preferably
from the thesi= s adviser.

Please specify in your application whether you are in= terested in applying for
financial support (details provided below).
Deadline for applications: **7th June 2024**.

Applican= ts will be notified by 24th June 2024.

FINANCIAL SUPPORT
--= ------------------
Successful applicants are eligible to apply for fin= ancial support that covers
accommodation and meals for the duration of= the autumn school (approximately
116 Euros per day). Please note that= there are no funds available for the
reimbursement of travel or addit= ional expenses, which successful applicants
will need to cover indepen= dently.

The workshop is supported by the Udo Keller Stiftung (Ha= mburg) and the COST
Action EuroProofNet.


Klaus Mainze= r
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.c= om/d/msgid/HomotopyTypeTheory/1d998bbd-5158-4550-a1dc-4caaa6146062n%40googl= egroups.com.
------=_Part_24145_381520336.1710220277197-- ------=_Part_24144_1020696311.1710220277197--