From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.101.102.17 with SMTP id w17mr5004635pgv.38.1515600863999; Wed, 10 Jan 2018 08:14:23 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.124.25.1 with SMTP id c1ls1577896plz.8.gmail; Wed, 10 Jan 2018 08:14:22 -0800 (PST) X-Received: by 10.101.100.218 with SMTP id t26mr5031876pgv.32.1515600862965; Wed, 10 Jan 2018 08:14:22 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1515600862; cv=none; d=google.com; s=arc-20160816; b=NiWfaBPv+mhZIH/a5hjDXlHrLitIVIj2RG8PrtiKHgaceVhCEkuI+eX+GoyNJuEpkw +ZPGRWcR0uhVZeOQPlG+nIBrbTBilH9E/ho6RyUPCJkCA8sAn5hmpsWFhsYSAmjSm5+y HpobXAmPI9US7e+Q1S4On7DF6P8s4CjaPHQJLUTRWtHVE9cO1xj1h1dEDb5Ev60LO77/ 97sgntIeYbAt4Ih3XIFIQ+ZlZY1jtltuQB3aC1CRedWOnbq3qrdyaRH6BL1eIxoIWJlA LfZC6h41aoZc3o2c6rnogi50SKQw0g/dWt5YirDnMMi1/WI+/KqmRboNBwL7LKk07A5j zNyw== 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=aBb38LwjsDCvQ8stdZQGZcSsFl5EDIF4Y1wO/4L/iQA=; b=fKtOuEzUGBQ0HoycmeVCayKA1IU8dxv2z7EJ/s3kJbNoK2nLTEn0SRFtUTzHEihx+6 tryEVyh3mrNS7PyL7ijn/h0AUPmYkK0OyKs3hlEcXkCGlB1Ik/S0IvV+WN86rRdfn9at uXruupfCJtYynM6eGIwaGfNDUbtz2/kE8jE0wXMJMub0InYQzp4IR8lt35gr+2q3lpF5 +MH56amM0DYelZwkuJRtWPyZxHAKwsBq4qgs6vxi204r7b6iBBEHxDaYAmk9VC5/se09 UvuOBGQYLJ3ORY1nRzDpZzgzNY+w/UI7et2vNkiAFy6NovsTRq3Xl28IESlwJH+nHzeH AVIw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=q1nHm8Qm; spf=pass (google.com: domain of andersm...@gmail.com designates 2607:f8b0:400d:c09::233 as permitted sender) smtp.mailfrom=andersm...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-qk0-x233.google.com (mail-qk0-x233.google.com. [2607:f8b0:400d:c09::233]) by gmr-mx.google.com with ESMTPS id d15si411797plj.4.2018.01.10.08.14.22 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 10 Jan 2018 08:14:22 -0800 (PST) Received-SPF: pass (google.com: domain of andersm...@gmail.com designates 2607:f8b0:400d:c09::233 as permitted sender) client-ip=2607:f8b0:400d:c09::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=q1nHm8Qm; spf=pass (google.com: domain of andersm...@gmail.com designates 2607:f8b0:400d:c09::233 as permitted sender) smtp.mailfrom=andersm...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-qk0-x233.google.com with SMTP id r8so19229307qke.6; Wed, 10 Jan 2018 08:14:22 -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=aBb38LwjsDCvQ8stdZQGZcSsFl5EDIF4Y1wO/4L/iQA=; b=q1nHm8QmaF30npTUDAh271Js2lhe3Jtd3IFRdhalT0MDjzuGAa6aSiLm57NfBM75YN GkVFIoJ8adIqcF94xyBdNkWaB+4wA94xLItGTpfFHYPF8JmyQaE0JrvxHEIGDYnG+WU1 jYurqxOjVlXqlIpDiVBeWWUXrEvKrspPOX42AGtsXLv0SlQomQ6cpji8ZPn47pkKhFch eup9smuNZHZXiljrLvmL9/GM0bjOMvx3Sj5jGatsabN7SOMHbzHKbEqvJvMdJdz6IHkZ 2TVaH1y7q0I0Upzfr2LKe3ixas3+bJ+PDhgw81WQUBNi8uHRL3RVWUqK56AMSrZhmuWR EiOg== X-Gm-Message-State: AKwxyteH94lo0c4QEldk+rScVQuAUqvSM1XuE5ZBQ9uJ+tkP4wixFkqr kkQLrc/g6owmwXljG0W76I6qJZNJlbjnoi3OnHQ= X-Received: by 10.55.80.7 with SMTP id e7mr28469457qkb.230.1515600862256; Wed, 10 Jan 2018 08:14:22 -0800 (PST) MIME-Version: 1.0 Received: by 10.140.33.131 with HTTP; Wed, 10 Jan 2018 08:14:21 -0800 (PST) From: Anders Mortberg Date: Wed, 10 Jan 2018 11:14:21 -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 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 ------------------------------------------------------------------------ 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: March 31 ------------------------------------------------------------------------ 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: March 31 * Author notification: mid 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)