From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a25:ccc8:: with SMTP id l191mr40818914ybf.137.1586214379068; Mon, 06 Apr 2020 16:06:19 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:25d4:: with SMTP id l203ls484447ybl.3.gmail; Mon, 06 Apr 2020 16:06:17 -0700 (PDT) X-Received: by 2002:a25:bec2:: with SMTP id k2mr39412524ybm.129.1586214377652; Mon, 06 Apr 2020 16:06:17 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1586214377; cv=none; d=google.com; s=arc-20160816; b=OC5GAJrq8bbvWe0hpG6Q+7uUqksYew8j+IfLjL41t1GCUUCbUV6zbtsr1KWcexbfhR zBMtKrOigWelRPuD8drlsoJhmd4mNYoI7ef1XIWXI8eyiv28VpK7ku+6zR3vjE++LSmU zTjL7Eq3KRiwZg4qx9hZSYfYifoPP8fYvPhxnq6vgrNPwzHd2irNcqxaxW9W5Ovva/oU Zal0HabW2gn7yp5fbUQVxH0fpg4FyDlCav+hsELYCfFS42Y3tdI8dC8ozWopa+UuYZb5 dmGgFInfOip7cZcbGE3iEgoFYy0EFMWn8GdMh6z9EX1eJ/36zE4ke22Nqna3bZX9ROqw r/EQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :mime-version:dkim-signature; bh=Ry7KfTDIAQk+f8jbPkve5enGu5MpsR24Vf88DjgDEZM=; b=hSszmjNvAfY2zUoYLD58T3cs4EFF3cz2uJ/+0BS6CzmJ9XmFek2gDVTqSf7jiLDCh6 mRIwcsjoEwIr3O4n3ln4/lN48yw1hLw/qgNy4NSVbdjf1PauxJjAfR/Cp9L0m2w6J7FM d4jLRAomh/HILht++38D4jd6YfMzQh4+qHIM6Ktn2hRBDnf8DrTrzavTVUWNCtuX3+r4 qF4Vqnzeduoqw/DqhCkYR/OUIJZh6+Vwuyh0PJB2gEP9qC/9rzoBELQKIOQNz4yUC6P7 HaVC3PprsD7aWzbx2LJkpWK8bj4vA/f5MtOsve06Sak0RXbPN+vQ/nLCyNwrgQCEgV7X Wxiw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Sj5WYrLS; spf=pass (google.com: domain of k.ka...@gmail.com designates 2607:f8b0:4864:20::131 as permitted sender) smtp.mailfrom=k.ka...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-il1-x131.google.com (mail-il1-x131.google.com. [2607:f8b0:4864:20::131]) by gmr-mx.google.com with ESMTPS id d72si106968ybh.5.2020.04.06.16.06.17 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 06 Apr 2020 16:06:17 -0700 (PDT) Received-SPF: pass (google.com: domain of k.ka...@gmail.com designates 2607:f8b0:4864:20::131 as permitted sender) client-ip=2607:f8b0:4864:20::131; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Sj5WYrLS; spf=pass (google.com: domain of k.ka...@gmail.com designates 2607:f8b0:4864:20::131 as permitted sender) smtp.mailfrom=k.ka...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-il1-x131.google.com with SMTP id f16so1255921ilj.9 for ; Mon, 06 Apr 2020 16:06:17 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to :content-transfer-encoding; bh=Ry7KfTDIAQk+f8jbPkve5enGu5MpsR24Vf88DjgDEZM=; b=Sj5WYrLS0uw/85LJDmrsf+QN1kXVPZpLuRuuyl9LB5IQrCPscAdGNrbhe906bbzgtY Fm8hhAIqz/VumCVROXZvkxfIAhiOvfZ14TYUj2baULtk8c09mli0WeAEYV1UmjDtcYsR MIHSyafom4RIclLIi3lx5Uz6oz01sv0pN7HJkaH9ecOaQAzFKrNY+yrCVbJO3wRi22Ac eGotAAvS9TAZ4nWEAlHmbSp4ygJc5nfsPKCR/Yd239ihCIhD3k7FjPtVswy1d4o0i5f6 hmuDUq27IfBAi8DUQSXfwDlgVyLCyRfjVtaygC6DBQgzGF0OYNNJNllRpDy6jQF/I9tV p8eg== X-Gm-Message-State: AGi0PuYRtVFLKb91MU8MoxsVfLqyv0/p8e+2JE2iBE9zfVe1U27Ovswj NahBjqWXq6kT4i06xsVKZSNEZoDeQa0yif/lONW60WuChKMMZg== X-Received: by 2002:a92:dcd1:: with SMTP id b17mr1937791ilr.80.1586214377146; Mon, 06 Apr 2020 16:06:17 -0700 (PDT) MIME-Version: 1.0 From: Chris Kapulkin Date: Mon, 6 Apr 2020 19:06:06 -0400 Message-ID: Subject: Update on Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF'20) on July 5-6, 2020 To: categ...@mta.ca, Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable UPDATE: - HoTT/UF 2020 will take place online - Submission deadline: May 20, 2020 Details below. Best, Chris * Workshop on Homotopy Type Theory and Univalent Foundations July 5-6, 2020, The Internet https://hott-uf.github.io/2020 Abstract submission deadline: May 20, 2020 Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory. The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory and Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. # Invited talks * Carlo Angiuli (Carnegie Mellon University) * Liron Cohen (Ben-Gurion University) * Pierre-Louis Curien (Universit=C3=A9 de Paris) # Submissions * Abstract submission deadline: May 20, 2020 * Author notification: June 05, 2020 Submissions should consist of a title and an abstract, in pdf format, of no more than 2 pages, submitted via https://easychair.org/conferences/?conf=3Dhottuf2020 Considering the broad background of the expected audience, we encourage authors to include information of pedagogical value in their abstract, such as motivation and context of their work. # Program committee * Benedikt Ahrens (University of Birmingham) * Paolo Capriotti (Technische Universit=C3=A4t Darmstadt) * Chris Kapulkin (University of Western Ontario) * Nicolai Kraus (University of Birmingham) * Peter LeFanu Lumsdaine (Stockholm University) * Anders M=C3=B6rtberg (Stockholm University) * Paige Randall North (Ohio State University) * Nicolas Tabareau (Inria Nantes) # Organizers * Benedikt Ahrens (University of Birmingham) * Chris Kapulkin (University of Western Ontario)