From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.117.10 with SMTP id q10mr34121400ywc.112.1507123735545; Wed, 04 Oct 2017 06:28:55 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.13.232.21 with SMTP id r21ls1045768ywe.13.gmail; Wed, 04 Oct 2017 06:28:54 -0700 (PDT) X-Received: by 10.13.201.198 with SMTP id l189mr34495611ywd.180.1507123734686; Wed, 04 Oct 2017 06:28:54 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507123734; cv=none; d=google.com; s=arc-20160816; b=O+5b/Afkb1Cb91/DXLAwirsAjnoUHcTjRlrhRFr8tv9sZhXxx8NqMiHqjyEqYv/ni7 D/q9NOFEzhYfesHTeM98rFpSjO5JQZMrtOOY0PFkKZLI+0sNXR8BfkM5cKprUEkVYvO1 aIKK74AOq5g+FXMHmD3DEXdGK3M6bNHAHuwK7utHT4ayc3AwXtBblAuWXuPIORCv59Mc 3dbfPgWo1BTYIDnpy3TplIr72DrtZ1CSmubHI0yN/Msj7QvpHB4iuHFkDMTxK2tc6TS+ gugktL1q8yyxX0y1sQz+GczuAe/bPja1ZefmUR1pvvsS4PCq7L70NLcOwy6djIFQVJj8 SdAw== 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=O8y5+ACsf4IxvTeJNRKs9QOdO7w03ATJO3OW1NElMms=; b=yvieuyfhl5pG0uq7IhuXEhhHIQ2owTEXFRd+Z2Td3QrhMM9Qc8c+6qo/nVEUsW+w43 /uYMgYcKJz536g+FaCVyervpKFxy9J9uE/Sft/Sqg1xCMcOQvRFdEjH5tiMh4OUydy9u RNQ1HJiRxuGq8zJwe9VoypKUyBH22LYOf+36sZIX4NK0llyPWhMS9TKEhSFVQb6iAAQ+ /3Zefj1gD7xwqtdP3Qnre2ApDj7JJcvmq/P6fubE8y2pG7SsG2l5VMQaoTR2lkROqEfK CRdQ7ZLdpIPKXpgJSX8Zfy0angk086XrumFPZb60fLlVn3DqvhZZrQX8plME9ZcWwQ6f wNdQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=UH2cO5xJ; spf=pass (google.com: domain of andersm...@gmail.com designates 2607:f8b0:400d:c0d::230 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-qt0-x230.google.com (mail-qt0-x230.google.com. [2607:f8b0:400d:c0d::230]) by gmr-mx.google.com with ESMTPS id u203si889006ywu.21.2017.10.04.06.28.54 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 04 Oct 2017 06:28:54 -0700 (PDT) Received-SPF: pass (google.com: domain of andersm...@gmail.com designates 2607:f8b0:400d:c0d::230 as permitted sender) client-ip=2607:f8b0:400d:c0d::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=UH2cO5xJ; spf=pass (google.com: domain of andersm...@gmail.com designates 2607:f8b0:400d:c0d::230 as permitted sender) smtp.mailfrom=andersm...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-qt0-x230.google.com with SMTP id 34so1953050qtb.13; Wed, 04 Oct 2017 06:28:54 -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=O8y5+ACsf4IxvTeJNRKs9QOdO7w03ATJO3OW1NElMms=; b=UH2cO5xJhx+RxHYcn7GvuDJ7MHrP+RzJ1Ed+RfCQJEWAfMWrZGXM5uWi2WLW7n3jVV EAayaEYGN+RmFAkbzfz0JhHRXlTKdacJeeyaqhux/e4hs34lduLuabjwGJOx92iCZqCy HJsfbMzJwyiuyL+2gKAMQTPI/PP+LogTaRE71vcosznzziXhfYPAYifQpeQtMWIOHfGZ 0LLQJWJX1qubOw+IzBJB/HHNkVyR8gmdU8xfKrWTxjeRf9sMU/VdkgW1K5pc/UiKbycQ CfA/oFemaOwtEEW/6R26P7Mc3owjgpTg8PgTjmB/aAtjZ8xVjVtVeE8LeMIbtoFskwl4 P3XA== X-Gm-Message-State: AMCzsaVzPTkYRtOVGcJemUTBzT9+w3VQGgUfeImXp0zIvhWygQDvOjps 9ak4dl2+H+O4hmpURoFXmIxhO9FI7L/DBbiS34s= X-Received: by 10.237.54.34 with SMTP id e31mr5656971qtb.328.1507123734233; Wed, 04 Oct 2017 06:28:54 -0700 (PDT) MIME-Version: 1.0 Received: by 10.140.107.74 with HTTP; Wed, 4 Oct 2017 06:28:53 -0700 (PDT) From: Anders Mortberg Date: Wed, 4 Oct 2017 15:28:53 +0200 Message-ID: Subject: Open call for papers: Special Issue on Homotopy Type Theory and Univalent Foundations 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 Open call for papers for a Special Issue of Mathematical Structures in Computer Science in association with the workshops on Homotopy Type Theory and Univalent Foundations HoTT/UF 2017-2018 https://hott-uf.github.io/special-issue-17-18/ BACKGROUND Homotopy Type Theory is a young research area 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 and higher category theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory. These ideas have led to many interesting developments, from the study of syntax and semantics of type theories to practical formalizations in proof assistants based on univalent type theory. The HoTT/UF workshops, co-located with FSCD since 2016, started out as a forum for formalization of mathematics in a univalent setting. From the 2017 edition and onwards, its scope has been broadened to encompass all aspects of Homotopy Type Theory and Univalent Foundations, in particular (but not exclusively): - semantics of (univalent) type theory, - computational content of the univalence axiom, - syntax and semantics of higher inductive types, - synthetic homotopy theory, and - formalization of mathematics and computer science in Homotopy Type Theory and Univalent Foundations. SPECIAL ISSUE We are soliciting submissions for a Special Issue of the journal *Mathematical Structures in Computer Science* (Cambridge University Press) edited in association with the 2017 and 2018 editions of the HoTT/UF workshop. Submission is open to everyone and not limited to workshop participants. Submission is open from now and contributions will be reviewed on a *rolling basis*, as soon as they are received. Accepted papers will be published on the MSCS website via 'FirstView' and will be citeable through a DOI shortly after acceptance - before the completion of the whole journal issue (expected end of 2019). Submission will be closed on December 31, 2018. For details and submission instructions see: https://hott-uf.github.io/special-issue-17-18/ GUEST EDITORS * Benedikt Ahrens * Simon Huber * Anders M=C3=B6rtberg