From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a67:906:: with SMTP id 6mr2689835vsj.47.1589167283627; Sun, 10 May 2020 20:21:23 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a67:c319:: with SMTP id r25ls954850vsj.4.gmail; Sun, 10 May 2020 20:21:22 -0700 (PDT) X-Received: by 2002:a67:1dc5:: with SMTP id d188mr9701513vsd.103.1589167282252; Sun, 10 May 2020 20:21:22 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589167282; cv=none; d=google.com; s=arc-20160816; b=FljEFgS815q9VpWGFm8vACim6pxcov2yTqoJXfUitA8sI1y4fCtT+yaooIzY+5OYr0 dO/3GMIWzopfsWn0fTuSu2mNPZns92rQsoc/0UiBDy/JLCz7Bu5DCDqWt+L3evNADqoE 25jxWnhwrrEsgmWU4Q4kwZKAPonB2ZZOBEjh1+i+4+I20UCT9grXZqZbRb6emsfrzBnx TQ1TWXNu3qrPJH6UjSgFuWQxUWQoBvQPAJ3Eq9s7MtNGS6Iqis7OVlZhrXZ0WzQ+TDM0 y69zJwB4QDXythewc8YW8RbCXm8mnkhQsrW9lDC9ng0OFyUcwawHq1JZbWmPyVkTFiQq TdTw== 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=y5re+dsPekX6EYieVhV2eNCAVnsuhOv5uOoDtPNxw1I=; b=jnNlv0XVI7gKcY0sel08dUiiosJvfO3IbYSWSPjD34VB5zVbMl1uF2VtmXpz5Dbxab HCMqkws6P4O1fmzjQSDmjifYpRjemrAN2BKDYODCPa/NHDP0aJfWCy5JvnJRh3BSwsJa hoTazek75Km/GIeTmcxNbOULfvIDsvv+E0V59kVFj9SrbZn7bBJgslvEkQzM2uuAiq5B cg7Sz+5V4QRwZ4xFj/VTR+SGLwyyhCFaE/9uUsI3Fk1DWDvpDn5F+7iKY5bTeYGOYlNb Yam37gPyWlhOpXW2nXdN3zyC8lnjOqJZfjZsNbxittyV7TbYT1yo41SbSnDQYTdEFTHz rUxg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b="WgUe/h0H"; spf=pass (google.com: domain of k.ka...@gmail.com designates 2607:f8b0:4864:20::d29 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-io1-xd29.google.com (mail-io1-xd29.google.com. [2607:f8b0:4864:20::d29]) by gmr-mx.google.com with ESMTPS id u20si383684uan.1.2020.05.10.20.21.22 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 20:21:22 -0700 (PDT) Received-SPF: pass (google.com: domain of k.ka...@gmail.com designates 2607:f8b0:4864:20::d29 as permitted sender) client-ip=2607:f8b0:4864:20::d29; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b="WgUe/h0H"; spf=pass (google.com: domain of k.ka...@gmail.com designates 2607:f8b0:4864:20::d29 as permitted sender) smtp.mailfrom=k.ka...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-io1-xd29.google.com with SMTP id j8so8006451iog.13 for ; Sun, 10 May 2020 20:21:22 -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=y5re+dsPekX6EYieVhV2eNCAVnsuhOv5uOoDtPNxw1I=; b=WgUe/h0HyWowl/Vjk2Wc5A72xxp8yTkuXtfGunHPHPgt4OPKKcQFoLR/PzOpzm/TrF OY8gN/bgfJOHfB/ZAo/1/jE3sFP3fqC85DTuMQdoO6pczoJniOhonlrRh+5dWhQsZ7jK ZgoL3AP/9AjZDAA1fb2Kazf16cBj44t3gXbm7UPm+ZbynIYuYPyRL8HEBYTiENfs0ywa 1POdzX/7YYDbfloijmIpWntGC3FtitN42BH+3ZPEK25JfyoK4NChjBB4+EhCyJx/zbQ6 JKz33Q00jwFSnLjmwjgdTVBu73nKZO4TYNANFtyA/l97ltxCdNDGkKcs7RS+sBNqT1kT XpEA== X-Gm-Message-State: AGi0PuZoRkB58rS4CXhFJ5vp/GqGryRkHfMsPM7amDfsaOEF6+YAQb6L uwZJK6PGKU57LnI1ffqoE5QjVxdPA7cvpeDyYOoQgsg5agEu8w== X-Received: by 2002:a02:cc16:: with SMTP id n22mr12764283jap.72.1589167281668; Sun, 10 May 2020 20:21:21 -0700 (PDT) MIME-Version: 1.0 From: Chris Kapulkin Date: Sun, 10 May 2020 23:21:10 -0400 Message-ID: Subject: Call for Contributions: 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 Quick info: - HoTT/UF 2020 will take place online on July 5-6, 2020 - 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)