From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.101.77.200 with SMTP id q8mr1236182pgt.161.1520013417446; Fri, 02 Mar 2018 09:56:57 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.98.194.153 with SMTP id w25ls3096438pfk.10.gmail; Fri, 02 Mar 2018 09:56:56 -0800 (PST) X-Received: by 10.101.82.4 with SMTP id o4mr1239981pgp.2.1520013416185; Fri, 02 Mar 2018 09:56:56 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1520013416; cv=none; d=google.com; s=arc-20160816; b=SRBfCLowfax593B+lgnUqNKH72QTLNEVnfK0bDgNcgnZWpbgxXdZw0kDJb38ZhqY0M ZDxleL+ZPb4FrZNy4De5SUYm++hVaniAIaXyt3QqM0g0N24fpfFGXKw7AGAUhg8DIV8N rSeSTIQK157Uw7TXzkS55idTROq2kc06XZAlE9HJxS8eQ9r50pgD6wjOTQ6zmwqrQJIe JqEUwdF0XqRfNlyh3qwGnmQy0vfwRIajNN1GpS5rOMiTUjjE1bkip43MNPuLiRlvKW+R j70fPvbBniURq7t7jPEqAbK3iasSSlNlw5NI3cTvhvsNnSOy71GAoQ2Fjsy83TgTbi9h fSnQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:date:message-id:subject:mime-version:from:dkim-signature :arc-authentication-results; bh=S3t5DDOohypnmF8eoTbBDXChtDjAJIrxX9yYae35G8A=; b=tho7H27io0QbExXPBr2kJjmxEmOqOk9f9SREl84ZBPY+4VEnRNOk5xMtPEVLFy9iKJ ocVLMqoThvArsldepWYUaPwHlvBAKLOeaKvLr0wTL+uDt2Unhj2lZCnKgJ5qLx7z3yb0 kYlf3z/X9FZ6t2aaUKfXZIXuPHq5l7R9Qw4V+Fkx4Hp+HPzl98wTDBAFNwOxzuXEMOqx Vk3z/aAFn/DS06bQ7jhHtfRRk2VIRX/jGRIjKIEuRCrfqhcDK1OCR/AUmmsO9vqECXFv 8Y8mhHYw7dO9HoYtqlkVDTSvs6H/QvcCPPSPaJiTXXlNFop3tgC2HQPcsEd+oYv5sGAn PB2Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=UKvdJuJc; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2607:f8b0:400d:c0d::232 as permitted sender) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Return-Path: Received: from mail-qt0-x232.google.com (mail-qt0-x232.google.com. [2607:f8b0:400d:c0d::232]) by gmr-mx.google.com with ESMTPS id p6si315654pgq.5.2018.03.02.09.56.56 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 02 Mar 2018 09:56:56 -0800 (PST) Received-SPF: pass (google.com: domain of awo...@andrew.cmu.edu designates 2607:f8b0:400d:c0d::232 as permitted sender) client-ip=2607:f8b0:400d:c0d::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=UKvdJuJc; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2607:f8b0:400d:c0d::232 as permitted sender) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: by mail-qt0-x232.google.com with SMTP id l25so12918467qtj.1 for ; Fri, 02 Mar 2018 09:56:56 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cmu-edu.20150623.gappssmtp.com; s=20150623; h=from:mime-version:subject:message-id:date:to; bh=S3t5DDOohypnmF8eoTbBDXChtDjAJIrxX9yYae35G8A=; b=UKvdJuJcuT9SKPTZPtecZR/C3SpcR1U0hGyFPHRDiFvrihTDJwpmmu0x/Gf1pUaage QhxNCWUJFAINowNDrt5FPeZalvlMNhNy4Y1x4TifC1jiO0QNmgc/kGqXO21Eoz4idaQa SlylJGsJq35xvPHyYY3Y97tIoYVAevtaRamMe/nmmO1R1TtNmSvwCcANKPndCSEhg0+M QugjnbaeOB9gdc1Xv6MT+z2DGcvN7V5ooeCMLhI2d4Ny051zdh6CETPNEQ7+ox6jRzt0 WxO7EfrTEINCBTxKpdncLQSaoRp5+HxRu1kyrkhXZRfLGGvJc0AWg7H0IbqluesVsCy7 7F2w== X-Gm-Message-State: AElRT7FzFJBHVK1xWlbkSEsClDeVaq0cMIIDFEQAuzJWXdBRMYEaDouL MV5R2Minxr6upEg+D8O8X39ArTEuQTw= X-Received: by 10.200.81.84 with SMTP id h20mr10067794qtn.340.1520013415210; Fri, 02 Mar 2018 09:56:55 -0800 (PST) Return-Path: Received: from samson.phil.cmu.edu (SAMSON.PHIL.CMU.EDU. [128.2.65.128]) by smtp.gmail.com with ESMTPSA id u37sm4992537qtj.33.2018.03.02.09.56.54 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 02 Mar 2018 09:56:54 -0800 (PST) From: steve awodey Content-Type: multipart/alternative; boundary="Apple-Mail=_A072FBFA-FA79-4345-97BD-23665F76E421" Mime-Version: 1.0 (Mac OS X Mail 11.2 \(3445.5.20\)) Subject: Extended deadline: Summer School on Types, Sets and Constructions, Bonn, Germany, 3-9 May 2018 Message-Id: <24B90B81-AAAD-4377-9FAA-A9FF3E05A42A@cmu.edu> Date: Fri, 2 Mar 2018 12:56:53 -0500 To: Homotopy Type Theory X-Mailer: Apple Mail (2.3445.5.20) --Apple-Mail=_A072FBFA-FA79-4345-97BD-23665F76E421 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 [Apologies for multiple postings] Summer School on Types, Sets and Constructions, 3-5 and 7-9 May 2018, Bonn,= Germany *****Extended deadline for on-line application: 15th March 2018 http://www.him.uni-bonn.de/programs/future-programs/future-trimester-progra= ms/types-sets-constructions/summer-school/ Venue: Hausdorff Research Institute for Mathematics, University of Bonn Organizers: Douglas S. Bridges, Michael Rathjen, Peter Schuster, Helmut Sch= wichtenberg Speakers and topics:=20 =E2=80=A2 Peter Aczel: Constructive set theory =E2=80=A2 Robert Constable: Proof assistants and formalization =E2=80=A2 Thierry Coquand: Constructive algebra =E2=80=A2 Mart=C3=ADn Escard=C3=B3: Univalent type theory =E2=80=A2 Matthew Hendtlass: Constructive analysis =E2=80=A2 Simon Huber: Homotopy type theory =E2=80=A2 Rosalie Iemhoff: Structural proof theory =E2=80=A2 Ulrich Kohlenbach: Extraction of information from proofs =E2=80=A2 Peter Dybjer: Intuitionistic type theory =E2=80=A2 Andreas Weiermann: Higher proof theory and combinatorics --Apple-Mail=_A072FBFA-FA79-4345-97BD-23665F76E421 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 =20 =20

[Apolo= gies for multiple postings]

Summer School on Types, Sets and Constr= uctions, 3-5 and 7-9 May 2018, Bonn, Germany

*****Extended deadline for on-line application: 15th March 2018

http://www.him.uni-bonn.de/= programs/future-programs/future-trimester-programs/types-sets-constructions= /summer-school/

Venue: Hausdorff Res= earch Institute for Mathematics, University of Bonn

Organizers: Douglas S. Bridges, Michael Rathjen, Peter Schuster, Helmut Schwichtenberg
=

Speake= rs and topics:

=E2=80=A2 Peter Aczel: Constructive set theory
=E2=80=A2 Robert Constable: Proof assistants and formalization
=E2=80=A2 Thierry Coquand: Constructive algebra
=E2=80=A2 Mart=C3=ADn Escard=C3=B3: Univalent type theory
=E2=80=A2 Matthew Hendtlass: Constructive analysis
=E2=80=A2 Simon Huber: Homotopy type theory
=E2=80=A2 Rosalie Iemhoff: Structural proof theory
=E2=80=A2 Ulrich Kohlenbach: Extraction of information from proofs
=E2=80=A2 Peter Dybjer: Intuitionistic type theory
=E2=80=A2 Andreas Weiermann: Higher proof theory and combinatorics
--Apple-Mail=_A072FBFA-FA79-4345-97BD-23665F76E421--