From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-wr1-x440.google.com (mail-wr1-x440.google.com [IPv6:2a00:1450:4864:20::440]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c45b6503 for ; Fri, 15 Nov 2019 22:19:50 +0000 (UTC) Received: by mail-wr1-x440.google.com with SMTP id m17sf9043903wrb.20 for ; Fri, 15 Nov 2019 14:19:50 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1573856390; cv=pass; d=google.com; s=arc-20160816; b=uQaCtF3cZ1Ca5lq10R6/0WYIY0iWdJolzhZwe7TdVb2NjgUrw6sN76HRf1c8bYJBLc R9Ux3ZlE5NBzbVNgca3B28cGEP9Mpt8R3e9+WQWKC2+sp69PuWbWPCaFTSNrjt8ddoib zP2rWqzgQ03lBRL9ZLZAs1YOQVhm1sKCYFybtFK/g43uJjf4VoMkcJNlQAOTN7vmlEVH PSJHgZbVMMD5IhDP9dFuiLPZcx8/pQbQTJodQip7AaFaQD3IqZPMv0OCSHtFJ+HHb1VW smb6tBBWEqqjOGao771b5DqmAwOcvi2koS4eZaPOsWcDR9rvcVVmswBngMevB45Us1NO WlOA== 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:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=Ev40bdY445rNTrWdRU69KljukEAkc10Jz0MPV0nMh4o=; b=rZ42ZnL4QRRBA/LuTv5ZypUjYJc7WV9iffCGl/EwM6dc/bsK8sHtjsI4IE6ydv6I1Z TttgpksezFxEEhIshzr/aJ0M81qf3LX6xqGtvXLHI0mfvopkj0qiNNNxAW5XmkxEWeoZ 1FE+kdcUpCxSomNXNxzY7LXBAQd7FkpuoCv3xPPki7Ge5DdaoXBNYyMBgKgOne5jytYJ 016oWFLwcwA6xBIMhzcKKDCDqBO74FLOJarlEabe5aNT+EIAXMNjEqrRGdt2wXQk80Lr NbccMJGksogi5NLmQIcuK7wv7v0xUUgusbMYpf4oUSPh+GjEUhezPSPdBXVcMb8hUHxO Zc3A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=NbYfAJDN; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::536 as permitted sender) smtp.mailfrom=p.l.lumsdaine@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:mime-version:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=Ev40bdY445rNTrWdRU69KljukEAkc10Jz0MPV0nMh4o=; b=K8/9RqorbKX0JPK4dgU124JquTr7IEA86g1p/mORnjnbGHAh812bZxwKFe/mxSGGp2 +MdcHRZHQDG7kydN9sH6vqpeQqa0rojd0uTA2IVBI9pzt3Ftanil31R2Y1LdXuGFRLwM Sa6MBs88ZvHKXMCTYXfPMHslrx1DSaLgNgaQZbdsjiUGr3793Ey3MghnSFkNYWoW2jwX sEo1T5SXVPdpxhDYFOIIs/sHLvt5eay+oaJox3vOa1CqGMRRxPu8bjiEmq+3FZJrf6u9 XPZ2UYrG8EhBbcXkwONKuqOF61lII37KwUY9CzCf3c6R7HbO/3CXSR5kCh3VigjrQpK1 ltpw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=Ev40bdY445rNTrWdRU69KljukEAkc10Jz0MPV0nMh4o=; b=g+pUrUPKUDfxkjO6a6ZSiUA9qMoE2xorqw2khxzzDODDwcx/IaquMWM4mUTBfysyiB 324TWAUvYCswT5GK6KdkJUzUeD0pKiN8k5SnRre+gsP7xZi93JBiSclNRgzNV7NknUSz GzwR6bysggj4hN92s6XaOUQaQkWzFAjDE4hvNbdjm7AF5Ecl66s1UzemCTQqCp40KTW0 6iQWMDBRf5t8O/vnilRoPSuvSoH2i6MyZzd7Cuk1pRvN8PKEFAUMwZL9Kw8KYZUA257q yeoixPpWmeVeUVU7fi4dvADMmTxgesq2tbWn/6y7iOQ38EAz65o9cJT2mWxVjXCH6zGF RbzQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to: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=Ev40bdY445rNTrWdRU69KljukEAkc10Jz0MPV0nMh4o=; b=n/f+R0JJgDc9Kiam5KtlTy3G0l0+W9nj+Kdgy3SEC2Du5QMB0GUlTpDHAZMcvqedy7 kvvY6Qr1C4quw0Csc4O80pWpaTElxy07WvoQ/sBI80IbK45ixhsJixlv0R++Zm6FEQiw oKsd0WcuTXIko1rA5kTbmpcYkXHrQTIaaqtdyyP/T5ViD/jrn5YrelN3BVSc5gdYgip6 uR5bBlCvglWd8ecCiZLHPOovaV0DDHZvGJmwCzTl4p2x0xiY2r8Yfw8wl3doahAgiRem QF5Sz1UG+yTgeCzrM55SYxX1G/B+VGCQQ9o7fk9DPeVmLOba9dsyjLjy550t/gWfcWth Xf7w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUIzS6YZmCQyAAQ7sBVnmDipZuYtOgo04NkNWFzL9oiZcj/Z30J aPjWk46bcigOjs93eZNFvPg= X-Google-Smtp-Source: APXvYqz1S5NpCoM2gPbOywoi/E0dOnGWvYII0tejIvW9yV4KGRBhbqFG35Tr5d4TpdvBgvtXxRzrCw== X-Received: by 2002:a1c:5603:: with SMTP id k3mr18763902wmb.150.1573856390363; Fri, 15 Nov 2019 14:19:50 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:82:: with SMTP id 124ls19461324wma.1.gmail; Fri, 15 Nov 2019 14:19:49 -0800 (PST) X-Received: by 2002:a1c:453:: with SMTP id 80mr17722886wme.5.1573856389700; Fri, 15 Nov 2019 14:19:49 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1573856389; cv=none; d=google.com; s=arc-20160816; b=d1Sr5f9xKRDSd5N/vCcr40LYsBHDnp5jbtrzT725rGjTGVIIxP05fXowiRjrnPmLio e26fNtaID6cOukYOFrx+Dm4m01YDSbE5608/6s4LCkDwO4AvpHQamxsBJ1R5gmaaC32Y +qWS8FBW5EoBzyGH9O78m4JElpNTPzwjyQY7EZpKMF/LdFDrNQ+E0XPr9xCxLFWN/kis Eg3MS2YWR2VawuFgm4OdByKNp7g6Hja6GdvGQh0mHsa1/3jz4Rx3w7QhJh6BmWgq5sAt F145Fj6TO7Hq1FyCNLHXjcPIKD0VXHuZ2/rxjKgWv7I5gffJP9kka35uictDk/TLHTo1 ubXw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=C8qO2kVwZZk7TRR1j0AtiJpnOYN3eNsEFFbabb8q4BI=; b=Kl9d9Bk1Rg/U0wWp9aTcGk4zkKILFIZB8zH6FAGh2Gw/JsxtydisHh+x39PH6FdvWL Dn+H7+Matryw5+Lt9UdJPVvtCSnvTbyPpMxpdOVEBLgzhNcufDLa+NbAKp69Hq/ccGV4 Mige/SSgOTysEFQ+w6w/pZatRk7xCt+T4yLEUnTj5mDUCcWIiAGqjWnTi0VBSEZf7UFx 8QNwB7MYkujHimY6/Mo1UHlbEXWhIi3RqsERA6PZwttnyF2RZ55GJ73HK5q7d0uVeKLQ xKwPnho3qvj058KPIA23rc4KGbzPRJ2N9Jk8ay+JI6k6exSRBq0rezbbrxs4hRufMpbq 4png== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=NbYfAJDN; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::536 as permitted sender) smtp.mailfrom=p.l.lumsdaine@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ed1-x536.google.com (mail-ed1-x536.google.com. [2a00:1450:4864:20::536]) by gmr-mx.google.com with ESMTPS id q73si320414wme.1.2019.11.15.14.19.49 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 15 Nov 2019 14:19:49 -0800 (PST) Received-SPF: pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::536 as permitted sender) client-ip=2a00:1450:4864:20::536; Received: by mail-ed1-x536.google.com with SMTP id l25so8700187edt.6; Fri, 15 Nov 2019 14:19:49 -0800 (PST) X-Received: by 2002:a17:906:b80f:: with SMTP id dv15mr4509487ejb.188.1573856389144; Fri, 15 Nov 2019 14:19:49 -0800 (PST) MIME-Version: 1.0 From: Peter LeFanu Lumsdaine Date: Fri, 15 Nov 2019 23:19:37 +0100 Message-ID: Subject: =?UTF-8?Q?=5BHoTT=5D_HoTT_2019_proceedings_=E2=80=94_deadline_extension?= To: "HomotopyTypeTheory@googlegroups.com" , Categories list , constructivenews@googlegroups.com Content-Type: multipart/alternative; boundary="00000000000000a507059769ff7c" X-Original-Sender: p.l.lumsdaine@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=NbYfAJDN; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::536 as permitted sender) smtp.mailfrom=p.l.lumsdaine@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: , --00000000000000a507059769ff7c Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Dear all, We are extending the submission deadline for the HoTT 2019 proceedings special issue of MSCS; the new deadline is *Friday 13 December*. Two notes for submitters: - If you already submitted for the original deadline but would like to use the extra time to revise your submission, let us know, and we will hold back from sending your submission out for refereeing for now. - There are problems with the MSCS LaTeX class file currently linked in the author instructions. Hopefully this should be fixed soon, but for now, don=E2=80=99t worry about putting submissions into the journal style =E2=80= =94 this can be done later after acceptance. Best wishes, =E2=80=93Peter and Dan. Original CfP: Submissions are now open for a special issue of Mathematical Structures in Computer Science on the proceedings of the HoTT 2019 conference, edited by Dan Licata and Peter LeFanu Lumsdaine. Papers on work presented at the HoTT19 conference are particularly encouraged, but the special issue is open to any work on homotopy type theory and related research areas. Specific topics include but are not limited to: homotopical and higher-categorical semantics of type theory; synthetic homotopy theory; applications of univalence and higher inductive types; cubical type theories and cubical models; formalization of mathematics and computer science in homotopy type theory / univalent foundations; and new type theories based on higher-dimensional ideas. To submit a paper, please follow the general MSCS submission procedure at https://www.cambridge.org/core/journals/mathematical-structures-in-computer= -science . When giving the submission details, select =E2=80=9CHomotopy Type Theory 20= 19=E2=80=9D for the field =E2=80=9CSpecial Issue=E2=80=9D. More information at: - https://www.cambridge.org/core/news/homotopy-type-theory - https://www.cambridge.org/core/journals/mathematical-structures-in-computer= -science - https://hott.github.io/HoTT-2019/ Best, Dan and Peter. --=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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAAkwb-%3DyOcx5dLEuG0vC5eTQq7EXY88LYZrTQGEmMf2BSU6e5Q%40= mail.gmail.com. --00000000000000a507059769ff7c Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear all,

W= e are extending the submission deadline for the HoTT 2019 proceedings speci= al issue of MSCS; the new deadline is *Friday 13 December*.

<= /div>
Two notes for submitters:

- If you already submitted for the original deadline but = would like to use the extra time to revise your submission, let us know, an= d we will hold back from sending your submission out for refereeing for now= .

- There are pro= blems with the MSCS LaTeX class file currently linked in the author instruc= tions.=C2=A0 Hopefully this should be fixed soon, but for now, don=E2=80=99= t worry about putting submissions into the journal style =E2=80=94 this can= be done later after acceptance.

Best wishes,
=E2=80=93Peter and Dan.

Original CfP:
<= div dir=3D"ltr">
Submissions are now open for a= =C2=A0special=C2=A0issue=C2=A0of Mathematical Structures in Computer Scienc= e on the proceedings of the HoTT 2019 conference, edited by Dan Licata and = Peter LeFanu Lumsdaine.

Papers on work presented at the HoTT19 confe= rence are particularly encouraged, but the=C2=A0special=C2=A0issue=C2=A0is = open to any work on homotopy type theory and related research areas.
Specific topics include but are not limited to: homotopical and higher-cat= egorical semantics of type theory; synthetic homotopy theory; applications = of univalence and higher inductive types; cubical type theories and cubical= models; formalization of mathematics and computer science in homotopy type= theory / univalent foundations; and new type theories based on higher-dime= nsional ideas.

To submit a paper, please follow the general MSCS sub= mission procedure at=C2=A0https://ww= w.cambridge.org/core/journals/mathematical-structures-in-computer-science=C2=A0.=C2=A0 When giving the submission details, select =E2=80=9CHomotop= y Type Theory 2019=E2=80=9D for the field =E2=80=9CSpecial=C2=A0Issue=E2=80= =9D.

More information at:
Best,
Dan and Peter.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAAkwb-%3DyOcx5dLEuG0vC5eTQq7EX= Y88LYZrTQGEmMf2BSU6e5Q%40mail.gmail.com.
--00000000000000a507059769ff7c--