From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.58.68 with SMTP id h65mr11595719ioa.132.1518966435650; Sun, 18 Feb 2018 07:07:15 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.123.145 with SMTP id q139ls1261773itc.8.canary-gmail; Sun, 18 Feb 2018 07:07:14 -0800 (PST) X-Received: by 10.36.51.141 with SMTP id k135mr9528863itk.19.1518966434347; Sun, 18 Feb 2018 07:07:14 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1518966434; cv=none; d=google.com; s=arc-20160816; b=fWhc6rmUoWhQATHu6e3M2doS8U9xfZA595lSLr34cPEdRrDRzDxBqtp8cKGUUNCePV FvpqM5t74mAUDIo9+ikZC3wfmINRWofSP4uHr+Gnqfd0Ts6su1dYmyl3O7+M6aBlMnbC FUHe0SiRXzzKtixdNzn3BOoV3bJLyhv1D+eJy4PRBvFGAzt/YAJbOfEThqG2+F3oE/y7 2uFI3gkAtG/ObQbyIiOY25WyOgayR/U0/t5W29Z3W1dDLKy9nPDhVVK0CxnFgPh3aoDh 3cZ9dPe1fE22uGbttV1TKNUEnD1VzF1ojIB/4xuc5RvS/ttm6/VJvgtGzu9Mv8Pz8Vau LDYA== 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=rv4UbmfYyagkTznvptsgYMMMlPNwGWH8ml9ekYucuqM=; b=mpBgn1Pjk2Avgyu2bEUHoAgNnSAZEISMAftv7SC2ucK0sP7CjHYGpEFlEELRZ5jWKU uCqVeBeL5BRacm57ndxZ3Uw45UvRM045Eq3sJWmdKdIhl5pmMbiVoJkSUkvyYxnJXUJG ftAHUBxiHs/MQFgrdKgErqa9negyfCFASAmtPu9OmDcR5t2pTH5u+GcRQnaX0jXK5HLt VHunf156GVL2D1jKxYExuwMMU4tFj/RfRo2+DfxAZL4KR2vH0Wars5vH4htWLFm689mA aa9Njd0jNBL4xD8lggEABZYJ49v6DblvRcsehVX9QnQx644KnQ1AOTQ3kpm6C7BZqTXm SXlQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=uFAz/mth; spf=pass (google.com: domain of andersm...@gmail.com designates 2607:f8b0:400d:c09::234 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-qk0-x234.google.com (mail-qk0-x234.google.com. [2607:f8b0:400d:c09::234]) by gmr-mx.google.com with ESMTPS id 66si1547400itr.0.2018.02.18.07.07.14 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 18 Feb 2018 07:07:14 -0800 (PST) Received-SPF: pass (google.com: domain of andersm...@gmail.com designates 2607:f8b0:400d:c09::234 as permitted sender) client-ip=2607:f8b0:400d:c09::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=uFAz/mth; spf=pass (google.com: domain of andersm...@gmail.com designates 2607:f8b0:400d:c09::234 as permitted sender) smtp.mailfrom=andersm...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-qk0-x234.google.com with SMTP id f25so9482316qkm.0; Sun, 18 Feb 2018 07:07:14 -0800 (PST) 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=rv4UbmfYyagkTznvptsgYMMMlPNwGWH8ml9ekYucuqM=; b=uFAz/mthtJj4wRjwEvHUTz6L4tUaI84CbCa9ueB4Kia5YoWyndQYRkZhmAqSwofrfy 4D/IXlpdqtwD5ds7uio72m0htrhNIjGa9H4+D40JyewEpOJpAEvmgEiHqpDRNisV7XV3 eFc9x4BFlmNsnFTx345yxqLEKtp+7j6CxAQ7YSzuyIuXjomo+qwqVc6O+KY/0IWGPM1B JJJjLAZCKWxBmrQoWN5atOb3ab6sH5xs9VXyopfg913VKy5UI3+Vw47oq54ecvUH8ads VV1DVFh9AczPMRfldPxMGoJbXrx6XJWknM5uY+Kd4bZk/vhZbESMqrh9KgntyC/3Xr6M gD2g== X-Gm-Message-State: APf1xPCSjenPQ1uKTzyNyv8BEkop083EUTcGoXGP6CWOGhA6sBEkzEqg rCBCYUu9QPgUWgq12QcSAyeFT70lJMV6nXusB0Q= X-Received: by 10.55.23.214 with SMTP id 83mr19886373qkx.262.1518966433820; Sun, 18 Feb 2018 07:07:13 -0800 (PST) MIME-Version: 1.0 Received: by 10.140.82.8 with HTTP; Sun, 18 Feb 2018 07:07:13 -0800 (PST) From: Anders Mortberg Date: Sun, 18 Feb 2018 10:07:13 -0500 Message-ID: Subject: 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 2nd 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: submission deadline changed to April 15 (was March 31) to align with general submission deadline of FLoC workshops. ------------------------------------------------------------------------ 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)