From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.169.68 with SMTP id s65mr1389275lfe.34.1502363987646; Thu, 10 Aug 2017 04:19:47 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.232.138 with SMTP id f10ls1938867wmi.26.gmail; Thu, 10 Aug 2017 04:19:46 -0700 (PDT) X-Received: by 10.223.147.135 with SMTP id 7mr845589wrp.6.1502363986336; Thu, 10 Aug 2017 04:19:46 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1502363986; cv=none; d=google.com; s=arc-20160816; b=MiOMD54e6P2s23Ru3rpfuwImsfX9AHc7Z8587sw/+Z0XcaziHCsDQXLj2NJB8ZSVF1 BqO7axFD+l89LRzDqW6fw60BCVm0UEpLdScnW0liGB2yVLOW+FTKa0X/8d2a5DoC6Qw1 wqmcPn85tmi11boCcEMttao09ccVhowSb9G68YzjMQp56E3Fa2SkwKLzfTYLv3e3B/sf TX3jA32CyWMKyoZrbPRmzqRTv6Mx3gN2Zntc7nH38sdKKIohYVi5On9by4TvASYCPvm7 7eroOSW9vgIMGY018RUF+ELo0qQM31VqugpcwZtMS6au66ZQ7UlwAgZOKRLoKjCWQzOb gINQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:mime-version:user-agent :date:message-id:subject:from:to:dkim-signature :arc-authentication-results; bh=zpCU8R98XinGfm3fxkRjo7VLovsVmj4r/4eBNHttNPU=; b=vwuJQTmPxQC7siqqarU4eSzPJ5hwqN0/9NXDdT/HmPKPseAoOSCwYLyuJobI/BQwhI 9Ubx7BTsMatZ7E12h7brJu4qFZ8PyHTSP8iuoSllqHMZAgjbf/zbSIbcX0e65NNCC8ti l7+JJn4kVjTk7MhQlRtvB26d2dsl+JjbaEUz8DoTM8ttwzf5uaPQKpFkufP11C2ntCve mViECfnKJM1tLkBWqWU9eBTxJVb6ARpqhmiYDtXmJZHoqnSxEziISVjSFFy3AQQaXY74 COg+0KkFJR2/7U97wdrbv/9E2Ru8Dt4PsfJ0eGZkPOk+6M/c1pJej9uvSZoh0uLPWDvU Mj9w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=L+Kx0kWu; spf=pass (google.com: domain of benedik...@gmail.com designates 2a00:1450:400c:c0c::232 as permitted sender) smtp.mailfrom=benedik...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-wr0-x232.google.com (mail-wr0-x232.google.com. [2a00:1450:400c:c0c::232]) by gmr-mx.google.com with ESMTPS id 132si1109318wmn.6.2017.08.10.04.19.46 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 10 Aug 2017 04:19:46 -0700 (PDT) Received-SPF: pass (google.com: domain of benedik...@gmail.com designates 2a00:1450:400c:c0c::232 as permitted sender) client-ip=2a00:1450:400c:c0c::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=L+Kx0kWu; spf=pass (google.com: domain of benedik...@gmail.com designates 2a00:1450:400c:c0c::232 as permitted sender) smtp.mailfrom=benedik...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-wr0-x232.google.com with SMTP id c24so1928171wra.1; Thu, 10 Aug 2017 04:19:46 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=to:from:subject:message-id:date:user-agent:mime-version :content-language:content-transfer-encoding; bh=zpCU8R98XinGfm3fxkRjo7VLovsVmj4r/4eBNHttNPU=; b=L+Kx0kWukSpc2cspucvDXrH71TJ/Gq3m3WMzjclGlKdnQzgweC8tp+G383XpNHOCjm 6JeV+FS4M0Wc56VgfnSwAtxgouYcTAGfQpq0wShPNVb8ZjFbY183z85AUjjUuqa4EyxP +cjIkSwyjWH/2VyXaeyLnCk3M+LC3pITNdX9EDBSl7/NF1HplgHVxpYBuj8xJhoQoDFH jfXqSNAppmxkS6shvY5xLdzACtT8M0iPzgM0CLAokKGS2PeW7tnpXEBu6wvjIpdjbpm/ 0KhSXcQjXNwnv0B2MRGZiL6RkAyXCuQmzk0yB8rpyu8YSholqW33MlGzl+uEf2dJx1lf 50yA== X-Gm-Message-State: AHYfb5gTPJcWQwuO4UsoOvY96ntR5DnYj9AQv61BNuQB2Eb/0lG8VQnl OLwQF+EeXSYlv96Ay0EgiQ== X-Received: by 10.223.161.145 with SMTP id u17mr7740585wru.44.1502363985739; Thu, 10 Aug 2017 04:19:45 -0700 (PDT) Return-Path: Received: from [192.168.178.63] (p4FF08C1D.dip0.t-ipconnect.de. [79.240.140.29]) by smtp.gmail.com with ESMTPSA id a1sm6090831wra.17.2017.08.10.04.19.43 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 10 Aug 2017 04:19:44 -0700 (PDT) To: types-a...@lists.seas.upenn.edu, homotopytypetheory , ag...@lists.chalmers.se, eut...@cs.ru.nl, Univalent Mathematics , coq-...@inria.fr, lean...@googlegroups.com From: Benedikt Ahrens Subject: HoTT/UF 2017: 2nd Call for Participation Message-ID: <73e412ee-27f1-831c-9859-adaed7fe8409@gmail.com> Date: Thu, 10 Aug 2017 13:19:43 +0200 User-Agent: Mozilla/5.0 (X11; Linux i686; rv:52.0) Gecko/20100101 Thunderbird/52.2.1 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Language: en-US Content-Transfer-Encoding: 8bit ========================================================== CALL FOR PARTICIPATION Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF, at FSCD 2017) September 8-9, 2017, Oxford, United Kingdom https://hott-uf.github.io/2017/ ========================================================== Contents: 1. Invited talks 2. Contributed talks now on the website 3. Special issue with MSCS 1. Invited talks/tutorials ========================== * Thorsten Altenkirch (University of Nottingham): Naïve Type Theory (tutorial) * Ulrik Buchholtz (Technical University of Darmstadt): Formalizing type theory in type theory using nominal techniques * Thierry Coquand (University of Gothenburg): Sheaf models for univalent type theory 2. Contributed talks ==================== Titles and abstracts for the contributed talks are now available on the website: https://hott-uf.github.io/2017/ 3. Special issue with MSCS ============================= The publication of a special issue in association with the HoTT/UF workshop is being planned, in the journal *Mathematical Structures in Computer Science* (CUP). Submission to the special issue will be open to all. Submissions will be reviewed and published on a rolling basis on MSCS 'FirstView'. More details will be given in a separate announcement.