From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCC3LY473AKBBDXHY7PAKGQESCKMAUA@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.7 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ed1-x53f.google.com (mail-ed1-x53f.google.com [IPv6:2a00:1450:4864:20::53f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 7d674eb4 for ; Thu, 25 Oct 2018 16:47:10 +0000 (UTC) Received: by mail-ed1-x53f.google.com with SMTP id h48-v6sf4985718edh.22 for ; Thu, 25 Oct 2018 09:47:10 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1540486030; cv=pass; d=google.com; s=arc-20160816; b=jS23BosU7D1/pLOUihRSSs83AcFDGFvzhxhxW81bbwFuWnHxa8UHgj/sHBKaNAOOND 8KrZLuqReS7K9ZSt30WSLpNPOBJhti3yVzPvGKeKBODuti0VXXnleVvIG6xKmZW+xKBI CmkToAea06Qn4F5CUlKpr1IWM4HE4vv/C8hM3ieZ4+T4PRmOFzUVkp5luRGteM0h+d3u 0eoPBCri7Q8DHUsCiN6Lpp2R1W6lrPHtC0oMS51/iNN9WFKX/+N88uxMvFwDUAOnMQvA LFDieBYfKXr1wU4pmxXf2yVigcf6NAocQlp0NpMKCQr1cZf1NbGLSagZV4OLoxcT+Kf2 HxSg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:content-transfer-encoding:content-language :mime-version:user-agent:date:message-id:subject:from:to:sender :dkim-signature:dkim-signature; bh=7NR3hPGZ7DbBmj00kxMZLpnlXRrNrVUy300X8pdTDNY=; b=xJ/Jw+zFN5LIrgLw+m0GMfi7eTabn5SsEd4ISI8JPNsegAcK35qreaT6b8I9oUv71U OndgzFVDzzX+m/tVN6SNqIin0y5PHu1N9GAGT5am1rUE2gY5nKaNmZthS/h707UZI5YJ Alf/1wPOfcRB0rF5dEh/RTbP7CPvy0D7y2/0ZhROYoVffTwhJBWFGDFOOzWtdXXmdbzO jJGaAzrndSF2K8UTewlFwIQl/tXaAD96OBJCITed8pIrwzoZLOgoFoZO8XXlIIbcMtfa gj8AEDkYypgqkE/lARcRmO9vSDrEz3qEdvwL4PtdL/y0EOE6niLkVITAl3MWKf2hMTp2 n8Ww== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=H1iYHjOv; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::334 as permitted sender) smtp.mailfrom=benedikt.ahrens@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:to:from:subject:message-id:date:user-agent:mime-version :content-language:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=7NR3hPGZ7DbBmj00kxMZLpnlXRrNrVUy300X8pdTDNY=; b=aqRJmUYhlb3SYkPKoco7vT5JWBXaNe/vTbUFjQPpKVY67E54SRp9UwwY7ATdaW+bms r/U2Jk7ItuhY/EvYNX0R83HMM0qNlshUs7ZaC5WQq6q4lY6NCwaM+pkYmXIWVWu7SNbM 4t7TPmsL/aoyCYz6VHbK5nXVg6BPrHsfVBqu4m9FoRDzWJ0o7yzuIaCxSTl9rx+JXq+h /0CbqqrD8YPuVwOOJrNXHRzHiYXaDHvj96UGL2/3QDO/gBsACvDm3nRZEtirUkioknG6 33XOHsg0XxGx/f6YFzD96Kif+msnfn6zz+4pyAYf5aZSP8/wHcltq/6AaGsDqLTeRXSD kQgw== 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:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=7NR3hPGZ7DbBmj00kxMZLpnlXRrNrVUy300X8pdTDNY=; b=ht1t4wXxxmwUa33h5zqLqC8Ctv26W1rRtm5NnQzRh6eNSdff/3Fzzwp+gtEi2cGzGU C7x7LoJaTKYro+UAmXiuY0rjh5sAdtLTMhx/cyuRXbLIrvprp72j57e4jwwslS62ikUo 4jLrkRCH9CJlZkh102UK3UQgCnjH/TXFdUm6TEkdkMdrCry7L7cQaJkRLvGjZXr8q3Rq +3auMe/tY8WCtWX/qtSak0FYdR3236cdu0zMVkreE1ysZpR3/RH7GMvJPbSbrBBGiKKO 7pWk8IReh8CD4wI2rULP4hfHYw2s4XMrwO9Z5zq5tdFs4as/e3vSiApA2Lxu8XMpzcw9 i2sg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:to:from:subject:message-id:date :user-agent:mime-version:content-language:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=7NR3hPGZ7DbBmj00kxMZLpnlXRrNrVUy300X8pdTDNY=; b=V1j2kLLt494Ur+IFYcFj285BN1oVlOO3X7kTfiftPtUmjkjyHJECo0ECy+y/hf3WBk QfrFhYArtjyv8eFoLX3nulG4tAbC5kQI3y1wMrcwnJIfj+5X3jCjLwCtrB6aXcqL+9PD W1OD5BztY9OzfrwoxZmJNKcb83rCutdT+QAMNQ2bH1ZNjQIqd69FXUTaPtkzPjd6piGr 5k0Qfusq/khfCatEPjz0poBAuPYJOfxtMD7OEMfrQqGFunSdfEwH7I5NgRrBnpCY5RzY zkMESwgRk7yEpRISrLvd6ZU0NTG9YEO2UQGEET9Tzakd7gc+SC0c4YgkopLiCZjhSq5u 15UQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gLjdZJpgYVvT1kIW0J/Eo0Jw0Y7oOoERhlnYIg0cJatLo5ucQpO 1jiOfK8diMdFCJ9WYSaXxEA= X-Google-Smtp-Source: AJdET5cSzyBo9DAREALDC52YxiuKJdA3pxvlbNFjbJec7A3j3nYjaSTK5XfCB6u7+QCgMlt/34DLNQ== X-Received: by 2002:a17:906:6ad9:: with SMTP id q25-v6mr39ejs.4.1540486030443; Thu, 25 Oct 2018 09:47:10 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:5fc7:: with SMTP id k7-v6ls890478ejv.15.gmail; Thu, 25 Oct 2018 09:47:09 -0700 (PDT) X-Received: by 2002:a17:906:f0f:: with SMTP id z15-v6mr1693eji.0.1540486029668; Thu, 25 Oct 2018 09:47:09 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1540486027; cv=none; d=google.com; s=arc-20160816; b=n3nq02CIEqOFSPoKjVf27oHYEH3mQ5vdmH21tXV+JK36Q5UpxDwypk5i6J5T4h4BLA 0iRjwRHM1UgrtLr7bdTrQg4rHlWtSP8q302pfpwZqSdtAd1Sc0mgvz+wRASajo1bNzfO ki22modHujW249dnAUrriVjpx1qLz5Sjvk6Qj3J1mDzWYj7y696Pot2W8egqUbP6ZNPb UesnBpfGdEkkEBlpFS9Mo8Sq0C/JUTnftixoFNkG0Y+czObsKKDwt4brRZZ+I/mhebrG E9OtUCA0A+6pm6CtHiet/v/bbz8CvihnBB6nYsx1jTBY7GWvufWlmPmT1BqzhzZF6wuz wkQw== 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; bh=+wV/qhQeVBntz1Edt9uBXUVB5cIUcPOf/yPhD/lOfVo=; b=VsNBmGEzafVyOjVxUQU8T+cRP4jsbxSeAIGaGVfr7Zu0tK3pc3FsUnHzMn6wicLQUS dxxAl24YhL8kTGqZztEx4wRcBog6bP+gXzf2w9bUUpwlpyUGGN6CPUZkozeBd4stDomJ YRkNLNLNQlC5j0ekt/TGH3h876yZ0gZRJlSQ2mrTo7UeGb47wRwbYs5Oq2e4A8zMJVR8 fQq+ZQVg51hKYlD2EoRG70T8O12wYtrSFEPTRxsKYpGVwWAtRazvs3ac6uJDJBqjyTp8 VHQKbGU+cJtK42uNWHv7ZwRuVo3RhiiANuoFrCyaCnZ97anlth53rUK2+MMW+1x7PTXV zwIg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=H1iYHjOv; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::334 as permitted sender) smtp.mailfrom=benedikt.ahrens@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x334.google.com (mail-wm1-x334.google.com. [2a00:1450:4864:20::334]) by gmr-mx.google.com with ESMTPS id m25-v6si199460ejb.1.2018.10.25.09.47.07 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 25 Oct 2018 09:47:07 -0700 (PDT) Received-SPF: pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::334 as permitted sender) client-ip=2a00:1450:4864:20::334; Received: by mail-wm1-x334.google.com with SMTP id r63-v6so2228493wma.4; Thu, 25 Oct 2018 09:47:07 -0700 (PDT) X-Received: by 2002:a1c:bac4:: with SMTP id k187-v6mr1221130wmf.7.1540486026240; Thu, 25 Oct 2018 09:47:06 -0700 (PDT) Received: from [147.188.200.206] (dynamic200-206.cs.bham.ac.uk. [147.188.200.206]) by smtp.gmail.com with ESMTPSA id u191-v6sm2052973wmd.31.2018.10.25.09.47.05 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 25 Oct 2018 09:47:05 -0700 (PDT) To: types-announce@lists.seas.upenn.edu, homotopytypetheory@googlegroups.com, coq-club@inria.fr, agda@lists.chalmers.se, eutypes@cs.ru.nl, univalent-mathematics@googlegroups.com, lean-user@googlegroups.com From: Benedikt Ahrens Subject: [HoTT] Open call for papers: Special Issue on Homotopy Type Theory and Univalent Foundations Message-ID: <0c8ee0e1-cb60-a0fd-c8ac-c1644d4fadc4@gmail.com> Date: Thu, 25 Oct 2018 17:47:04 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.0 MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US Content-Transfer-Encoding: quoted-printable X-Original-Sender: benedikt.ahrens@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=H1iYHjOv; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::334 as permitted sender) smtp.mailfrom=benedikt.ahrens@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , 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 --=20 You received this message because you are subscribed to the Google Groups "= Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.