From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.120.7 with SMTP id t7mr6743341ywc.146.1523202276555; Sun, 08 Apr 2018 08:44:36 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:9942:: with SMTP id n2-v6ls445277ybo.18.gmail; Sun, 08 Apr 2018 08:44:35 -0700 (PDT) X-Received: by 2002:a25:cfcc:: with SMTP id f195-v6mr4835427ybg.29.1523202275810; Sun, 08 Apr 2018 08:44:35 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1523202275; cv=none; d=google.com; s=arc-20160816; b=NeP7v+hEBWyOplpEoX7kxpEL5CGgc0NZ520UJa1iGUoijhmzcmZLHjGdoOxzsUT/Ic skU/qG9a7AMApim57L16Lgty7jNF89hkKW+CuUhNlnuRff+7dxo+Vbx6Sq+DV+VN22I+ 44WnUNPUxBs7nG69erP8/o754IECoe8LwfMb538Wx4RR1IcVoCOPWxytWEMnStCparzL W124mdyVl/8bw0CcV4wdEX+AEcHOOHoJ7Ija1y8fd24qCIJuA6w43esPfthJrmjYlXNU OE9ndaFZBhJZMiIkAVKrP8awfmWb5EZ/xRIhIAyphgJ9B1XyioIfwRU3ovejAsmuPD53 PHBg== 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:arc-authentication-results; bh=6W2HOfkcbWLn777u/dWc3Yvk68EmvpYf3io5EJxd0lw=; b=sAri32MWhMW2kmxL8LPE26zYvyhe8tld4PbP2PlRHEn/BdsDBb8StYvjcgOhAyxlC0 AilzKEQBe7zi66Vd8Qg1R9KWHsfl8Ci5IC9/nUBsdVMA1exJkBmQC911g7/y6DvUgdAU HyQvtP431SkSnSW7/UKDedIHgiD4jxN2Y0EBml/nfL/yNe49SD4Rv0OoeYJCXTocicp1 h3Pya/H1D97wILANubSrIu721kcD1fqm2gonH6cCCHM8wcCa/d9sZnTVgpyI7AAKKmQ3 gknu34ny5fEKqnn+1SYshhlAOOcidXXx9YWfGdhLo6ZfJPixSbh6sa2zPDA/x+8V+ySE 9c8A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=jXCZwT5A; spf=pass (google.com: domain of andersm...@gmail.com designates 2607:f8b0:4003:c06::243 as permitted sender) smtp.mailfrom=andersm...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-oi0-x243.google.com (mail-oi0-x243.google.com. [2607:f8b0:4003:c06::243]) by gmr-mx.google.com with ESMTPS id w64-v6si821847ybe.5.2018.04.08.08.44.35 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 08 Apr 2018 08:44:35 -0700 (PDT) Received-SPF: pass (google.com: domain of andersm...@gmail.com designates 2607:f8b0:4003:c06::243 as permitted sender) client-ip=2607:f8b0:4003:c06::243; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=jXCZwT5A; spf=pass (google.com: domain of andersm...@gmail.com designates 2607:f8b0:4003:c06::243 as permitted sender) smtp.mailfrom=andersm...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-oi0-x243.google.com with SMTP id u84-v6so5373511oie.10; Sun, 08 Apr 2018 08:44:35 -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=6W2HOfkcbWLn777u/dWc3Yvk68EmvpYf3io5EJxd0lw=; b=jXCZwT5ALC5ASeYycwKTdL8F+SPN9k3XTRa6LOV3tjuatzL63ZrT0CNQ1WcT38rVsC 7tqdGwiNNFzJWx1PgZlWS5lhrvSGoWqRtOAbIV/EFL3E2fdxAwBhf1qLRlaIB4RcBBxV g54NOEeAJaEAL1Qa+9LegsjfN1XXpxT1iBwG0gmbQS6AQrnxJcsgOYen2djaQTilr2C1 +qXmhu/f3VC9p/Fi/USidlVUxzpoRfIhYJZrwBO3IJDmE56KmTyIHGSWiRL/wahRiK1W Ef/P6DANqO+kyPEVqN/jnWC7xFeTmOlkjnidRmwHQ0VQT9FX7amagHY0g7088tR39bys /4IQ== X-Gm-Message-State: ALQs6tC5cA43ffInJqQJR29Xe0qWTg/vWI09HNdx5fZ2Y+44K7bDyxAM 86uNZfs96WhWDo+rQN0kjO6qYp/xkYQHOQAitSN4fA== X-Received: by 2002:aca:acd1:: with SMTP id v200-v6mr20530930oie.320.1523202275315; Sun, 08 Apr 2018 08:44:35 -0700 (PDT) MIME-Version: 1.0 Received: by 10.201.108.213 with HTTP; Sun, 8 Apr 2018 08:44:34 -0700 (PDT) From: Anders Mortberg Date: Sun, 8 Apr 2018 11:44:34 -0400 Message-ID: Subject: Final Call for Contributions: Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF'18) To: types-a...@lists.seas.upenn.edu, Homotopy Type Theory , coq-...@inria.fr, ag...@lists.chalmers.se, eut...@cs.ru.nl, Univalent Mathematics , lean...@googlegroups.com Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D FINAL CALL FOR CONTRIBUTIONS Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF, at FLoC 2018) =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D NEWS: 1 week left until submission deadline! (April 15) NEWS: FLoC provides travel stipends for student attendees of FLoC=E2=80=991= 8 with application deadline May 18. For details see: http://www.floc2018.org/travel-stipend/ ------------------------------------------------------------------------ 4th Workshop on Homotopy Type Theory and Univalent Foundations July 7-8, 2018, Oxford, United Kingdom https://hott-uf.github.io/2018 Co-located with FSCD 2018 and part of FLoC 2018 http://www.cs.le.ac.uk/events/fscd2018/ http://www.floc2018.org/ Abstract submission deadline: April 15 ------------------------------------------------------------------------ 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. =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Invited talks * Mart=C3=ADn Escard=C3=B3 (University of Birmingham) * Paige North (Ohio State University) * Andrew Pitts (University of Cambridge) =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Submissions * Abstract submission deadline: April 15 * Author notification: end of April Submissions should consist of a title and a 1-2 pages abstract, in pdf format, via https://easychair.org/conferences/?conf=3Dhottuf18 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. =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Program committee * Benedikt Ahrens (University of Birmingham) * Paolo Capriotti (University of Nottingham) * Simon Huber (University of Gothenburg) * Chris Kapulkin (University of Western Ontario) * Nicolai Kraus (University of Nottingham) * Peter LeFanu Lumsdaine (Stockholm University) * Assia Mahboubi (Inria Saclay) * Anders M=C3=B6rtberg (Carnegie Mellon University and University of Gothen= burg) * Nicolas Tabareau (Inria Nantes) =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Organizers * Benedikt Ahrens (University of Birmingham) * Simon Huber (University of Gothenburg) * Anders M=C3=B6rtberg (Carnegie Mellon University and University of Gothen= burg)