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=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ed1-x53e.google.com (mail-ed1-x53e.google.com [IPv6:2a00:1450:4864:20::53e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 20f94e4c for ; Thu, 17 Oct 2019 11:52:45 +0000 (UTC) Received: by mail-ed1-x53e.google.com with SMTP id y21sf1306791edr.18 for ; Thu, 17 Oct 2019 04:52:45 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1571313164; cv=pass; d=google.com; s=arc-20160816; b=DQLVt0xg8ES+uAt9CLs/fw7OAp/7jE3rJjl6ltgttI4vIEyG6Rl3bpeIh4uGy1bMzK HGSxYhKeqxe9qP+4fCY8KfCH+WV4mko2q/Sx3PIgHh9dRBXHH2kpmnS8f4jpx99hmPUp wZ3kxNNn/dZeHrHnnMDM8EBlrx529IIfgcJjS4geEw4FMD/+ARqmEOECPSxRlT42sFW2 UwjSrezL4HhGcpJqZflsz19AqpqCs9zIYttro1IfT9EI22ym+cTk9zAC/0cTDoTfEsvB ajbr+Av4XToboUf09y0lhuyEr3mn34Guc9/DnzWhgG6ooybeiha++6wCE7V7B3OnkC+m ZvWQ== 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-language:mime-version:user-agent :date:message-id:autocrypt:openpgp:to:subject:from:sender :dkim-signature; bh=j2JgSGpcjnc8s1rFnEPUcFj+VK63vA/BMoJqKmV3nx8=; b=Svwl1DwabFQp94D/fvaxY+gUkoPd/VLwXJR9WSMaxQSzvctZ6P6KK/BUi+si2pUbtA Grz/dRRzib4/JjXGtVvL+nkW1jawwltssicoz8SeAucPBqJUI987wQkqnJX9iE8DyOTU +7U/cazN5VZq7H0mURR7w/qmDv0niLbG/RGHwMUl9typ3DRJodzWBX26K1du4ovAhHLC 4q8MM495URCPKThRf4+iNMW7ZXdueWNGurFQUUnUJVxw6JB5eGYcEZWzYPv3BcKyI32g 98nx6Bcckw7ualuTUI9saYazi5Ati6W/XpsVkejhP+2jBC6X6EbsTVkDc1p7pU/dhj19 vHcg== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of assia.mahboubi@inria.fr designates 192.134.164.83 as permitted sender) smtp.mailfrom=assia.mahboubi@inria.fr DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:subject:to:openpgp:autocrypt:message-id:date:user-agent :mime-version:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=j2JgSGpcjnc8s1rFnEPUcFj+VK63vA/BMoJqKmV3nx8=; b=TYoUTRXqHmLAx7KQFPLF/wZqfWbehnW8htXBNp13DRxI0BDwVNRWF51Y268ALt+009 Fn9xZFk63Jt8JeFYKtyMTIGFveuIXiR1Gn9QFptzcxkUp4K0SvUXV8wskFMlni4w1Ud+ 1QnSXjS5CKnWA2Qw09/lGEfl0mva2DT2F7yp8zWS1zxKUFfCEo2GpWbroRIMXRBHRWKe NFuyZ93m6A6btBZXVHmPeD82JrfkIXUoZW6mm6DKi46m2UOaCCqrdl+pYJolKNx9B++f T84GARl0owz/WqV2wIgTfdqbxpup76053HHvOVd24tg29EJbT+6nlHKnasd5sBbcKtXb 1h2A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:subject:to:openpgp:autocrypt :message-id:date:user-agent:mime-version:content-language :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=j2JgSGpcjnc8s1rFnEPUcFj+VK63vA/BMoJqKmV3nx8=; b=MZ+Y0FhM9N0Q+pp40cVsS7EXA6F/3jJw+fajk00gQ29NGjAd0SgRg/3usmq1K3doQa NS2/NpO4h8X2dTS2ZuO5Sx4HVm9ovYpqcP5NNRMgK8wEAREfOaPLRwXAfApArK1BKC9K qE7gv2eUvJiBg0GWagmUZp+puKzKFYIXt1qBhVs2pu6vxh/Rn2LN5eTxgZZmCJkn/qoK 9NE0hptjd6CHXnw1os5VxBvFs7AAcPlBGmIjPn/C9AmgtQrt4ybBmvRdPWKWTnOzLUy4 OtHpIn8wk8pBeIbErqKYMTDhPjsAOslhEOQeVJL7Fe08OeqDsuILtdPNCzkue2RjcI03 IjJQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWuUPmu9QG2Msf54A+IkJMhmGjbE2/umiSc6x/R4pbfRU3rBxue x5LQRbmC1aL5RYcgvHQrEWU= X-Google-Smtp-Source: APXvYqzVgTyUg0F5Zp9lsAqhjSQh8P6g1FX4ZeE9ovQTn14RzyUZRO3dtrRSczzaYBtbq60I3hz83A== X-Received: by 2002:a05:6402:b02:: with SMTP id bm2mr3287985edb.244.1571313164635; Thu, 17 Oct 2019 04:52:44 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:ac7b:: with SMTP id w56ls498691edc.16.gmail; Thu, 17 Oct 2019 04:52:44 -0700 (PDT) X-Received: by 2002:aa7:d04a:: with SMTP id n10mr3368285edo.14.1571313164157; Thu, 17 Oct 2019 04:52:44 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1571313164; cv=none; d=google.com; s=arc-20160816; b=F18ujhYcfpc2PE9u452+ls5XoZq7R8J9i37bs4P/b3Ukzrrn51eIMUootn4AT9UT6I yaWQhor48vkjfkrc3Yh1b7lhW4JGn4ip6rhMYtwpr/6B1obYdUo5HhttWelpDMaRALV1 rTBCcRCgzNcu5/k0IyflssuilpNTfu3jGs3PYcNw/K9jMI9MSUKuladCUPOfQAALIxkU ZU3Ds089lTmG7tZelbnpsC+i2w2QBYT6k1y8oC+yayQ8hCZpciDK7rly13ttpPT0Ythf rKBOyQ+JLlEWLHq8u9azV6AQ237Ty6bM9Bs5p+kh3FDfhKLxXvviGafp0V60JxfHH5Qt jtPQ== 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:autocrypt:openpgp:to:subject:from; bh=xc2ytu5ZyG6HrLHl/M4Db9qTSwrOlICmg4MfYiEdgKI=; b=nvtRSsbH5N4nm8Rqx1eImyiqfEmyDc03i7B5PvsNcFeA7hNiWIsXVvNKRz5TgWKWlh sMq9QmGegoTsSHLpPbmc2SYpql6lPUZn7VxeUJCOZt1OPLO0FcjSeWWgLx43rLCk0YCo pxndEExZjjdvXsJ+UyXwGoLaTUsIN66Iv5Pb1QiLJR6ioOaVBOddgj9DGqAgOAa1Eihs Q2c3fuREmMFOz7F0aC2+As8d80UIEjNYkXZnDpKT4U5qy4nUyeCnf3BhM6tuanQ6NYiu ieHyWDTf81PfTWbzzW0unfdV4ygmwkmIJ0v2h76BvGynPvR53C5gHK+XGSJkoFC9CoBU zLYg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of assia.mahboubi@inria.fr designates 192.134.164.83 as permitted sender) smtp.mailfrom=assia.mahboubi@inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr. [192.134.164.83]) by gmr-mx.google.com with ESMTPS id d14si119019edb.4.2019.10.17.04.52.44 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 17 Oct 2019 04:52:44 -0700 (PDT) Received-SPF: pass (google.com: domain of assia.mahboubi@inria.fr designates 192.134.164.83 as permitted sender) client-ip=192.134.164.83; X-IronPort-AV: E=Sophos;i="5.67,307,1566856800"; d="scan'208";a="406612308" Received: from unknown (HELO [172.28.33.39]) ([193.52.83.10]) by mail2-relais-roc.national.inria.fr with ESMTP/TLS/AES128-SHA; 17 Oct 2019 13:52:43 +0200 From: Assia Mahboubi Subject: [HoTT] Open CfP: TYPES 2019 post-proceedings To: Homotopy Type Theory Openpgp: preference=signencrypt Autocrypt: addr=assia.mahboubi@inria.fr; keydata= xsFNBFRwdNcBEACayG+RJjOUz7A9KI4UJZQ4rF53F/QbuWsVwxs+HnFaMHlGA+dyL41hOe14 B+4w50e2jHy6KaBKLP4HFVZpJKpWQsxRmP6vREpbHziF1aNNgoQAER1iriqOiNNTZG8Nbvre ve4BwVHBmbblDvqfXvHdBh35KG//kwYCwAz2g05FWNKe7OZhrQ0wjsdh9p9rSm9mSgL4jFIH 7FxpFw3I20jr+qlTXUyFHLXVjFZnxhznOGa8Kwp3o+UfkjRNUd8bBEbz+jtz1XHTbmDbQRrt msUNozyryiu2mWMt26fJZbSrk6fR/IV/y0XoTe6Uz0o2GtnjeXmCFxe7DwZtwVrina90+MuY okXmKVmv0JVlP3ic1m+GDdF0RNTh0r9w666YUmhebjgwR/3I7uc2JLHJCM9LulnQWx6aVJhH WsELeu5hLXgf9judAtZxUc8aZx7l8I4C2UDRbdSBqQTW1zhxdb6B0TCCuiNUqCISXG6xKAqm 9PsU6Ohb7rIal/yDmy4or/IclxRXx9W8WOxJxTZZt43GyK/1hS43UP6fI//V5cVAOilzOLlc iCdWtlHL4xv+gboSAAH7W1GoZyhpGKb0L3U/BhO8tkTtSPQx9d/GflmHxNBiQeccVAtEYIy4 knIrCuetxksGyZ72E9fXE62tJhwoxlCg6JvOEZAEXzHxbVfywwARAQABzShBc3NpYSBNYWhi b3ViaSA8QXNzaWEuTWFoYm91YmlAaW5yaWEuZnI+wsF+BBMBAgAoBQJUcHTXAhsjBQkJZgGA BgsJCAcDAgYVCAIJCgsEFgIDAQIeAQIXgAAKCRBWO2266JVxsV95D/0bWtsjZ1vjuZYkqR0r WVIs2/G7yYMZ24TGO3EAe/VjXkLlIwyQnUTzN29q40m195zJml99BVVrwsZD4gbV+fu2TdTC YKhgRx05IjeGvcwiOYSplrGUHWg2WN+ofBaHPLeugCmKGBIXCpKXoWS79+amIRsaemVyJB9J P6pvrHfjKXtWaL4JRlhycWv+AeuxA9YVbD/lHFdd8uG/uizIXhuammFov39XKQMujrbejNS3 GggU0XE2vsVQa1ERjgjfk64XMxn1wiXQV9KFSbcSHzSiV8i8he/Ho+xEr/ATnS5cOuK8foUf dQS8yoGQwThHMuV+yuG2d1GSnBW9qTR1x7qNf6DAEQYw7XYYfeggB50Rxe7MS2bf8sj5q/4N tB7AyJT1hcdK+v+Pjr2AjVpX6kwLdLSauLcBpp36qYhpidygQDLV3U2+IbjTrEejgHxuOs6r 1iWtMNppoezyP7IbK0wOZ+RwGE1R01blj8geOm/d5QXoRr7SHocnPyq8Jbi15g5JxTZAFuHS UxaW8k+dGsH0wQxuEcF5JTmM+2kv95Wf6W/jueU2oPt3jQnNWtYu+368scJX882tEJTfkhev 7NbXvsWFpTeK9sqftMW/1dSOkcKpHySECmTQVst8jIMLdIPLuRECBGrrzz9Gx+Pwv/MwVDLR lXOoPSK1pmx86bT47M7BTQRUcHTXARAArjgoFHzZMjM6X7AxO4aTMk+feBC5sFokah2TYdXM eDCR4SbUwNDTgBMi7JtKaUgFW4jh1Hj9NiJJHimejixiho+ZIBJdAwz+auJZVX4RL0a9gSxz hCBT6XRNckUjCJyH17ebzGlPQwgeolOJky063nVOkFmcCLInnh0Q0zbEeZ0RzwPlvNMw/F/4 WOhMQwlifIpIG/jREqcCQzNcddCsZSt9FNIGx0vlGEn5B5lvkM02fbN35/BOf/gKDYbjjgjH HJvYyKnNRHyzL6WNzJw+dKtfr1SvZ5Ms5YeY/CXm3/Xxq53MnoT0HGpjoij3o53toTdnV09z euYWlURq5mzcncSQsD+R7hlv5f2gfmDwLYQeDIwljmjVNXHnYaYtWNghiMdR5sIJvKBqB8tu 25WZd9AaqysnNEokuQi6tfbix5Am4W9J2K7CWzNT7c5n/sBbS5OJsGOW66hck7VAhHVsFjxz Wmmy2C2pIx5w3iJzrzGJlI+anaK/XxJowM5td2faiNZ5wWfVj5lkCJeEqRyAT3INz+5zPsin yQ1vU44JU6C4kjsYBhQ+2YnorrWp2ceRqg483gPYdB/d1DPjOt8j4pIqh2vbhkIo+V56owdt /yerQY1Ykn7zLJ3k/jstdXDF7fXQyFrPMpDnvzG0Gyd79jKNW6M+Hf+1wn2Y/j4YDyMAEQEA AcLBZQQYAQIADwUCVHB01wIbDAUJCWYBgAAKCRBWO2266JVxsWnED/sHj5v9vOCvf3jvzqfz qOrBIuku8M6sRPZcZWtfsXote6l8G3cso6qpNzf7LJmEqfBe4kOMwglgs0Q3osYAr7i6Fjid Qbfbx973gorst7tVek7t7i/s+HOsqW29qocNCa0uysinWjlruC/GaLbCWpcRFPWIcMyc9pCR GiHxUhqVIutwD2K0uTIjQDZzISKkZG+hsUedvlm4tS3gmRNWjg4G2xISgyJ0/AAzkP8O7riY jWZ7B1ih0WkKccBYq5BHs/JkKYuIfYww2DxlFuVbWxyi6yLulu3w4J9gNOBzRzBm2S3hggAX FUq1QHdMrTECoSQ/KioDUgcBJ1mqM53r8AgoTUBdKU8OEriGeusNvmOBA++SjQibdQTaNsqS A6m1uCcyIhvmcGHIecS80z5BftC9hEfzGTVepBwF71Qdj1UyrNkouVdRn2tlFsTF72RgMdfl Q4C15ux51RmUL9hGDYoDHFXS2TxV+0keqRsUBN7WKY7ZscTVzoeeLekr98foMXL6cECPCzQ6 d4rv+2mL8653OOcpm3KkZQy7fnmdoqo97RIzOaVo56RvI97zu7w2to4bERdRphZwwMJDv8KE AJq/P7Wp/STs2XD6wnPjGLLFikTvE/ujE5NSS5KVM3M9TdfdYO5gOQ2itiT3DU7J5Wionw4A jk5NNWijOhe6shDkUQ== Message-ID: <7883ba07-5dea-8bcc-673c-5bad76377994@inria.fr> Date: Thu, 17 Oct 2019 13:52:43 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.9.0 MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Language: en-US X-Original-Sender: assia.mahboubi@inria.fr X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of assia.mahboubi@inria.fr designates 192.134.164.83 as permitted sender) smtp.mailfrom=assia.mahboubi@inria.fr 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: , TYPES 2019 post-proceedings submission deadline: 11 November 2019 Open call for papers Post-proceedings of the 25th International Conference on Types for Proofs and Programs TYPES 2019 TYPES is a major forum for the presentation of research on all aspects of type theory and its applications. TYPES 2019 was held 11-14 June in Oslo, Norway. The post-proceedings volume will be published in LIPIcs, Leibniz International Proceedings in Informatics, an open-access series of conference proceedings (http://www.dagstuhl.de/en/publications/lipics). Submission to this post-proceedings volume is open to everyone, also to those who did not participate in the conference. We welcome high-quality descriptions of original work, as well as position papers, overview papers, and system descriptions. Submissions should be written in English, not overlapping with published or simultaneously submitted work to a journal or a conference with archival proceedings. The scope of the post-proceedings is the same as the scope of the conference: the theory and practice of type theory. In particular, we welcome submissions on the following topics: * Foundations of type theory and constructive mathematics; * Homotopy type theory and univalent mathematics; * Applications of type theory; * Dependently typed programming; * Industrial uses of type theory technology; * Meta-theoretic studies of type systems; * Proof assistants and proof technology; * Automation in computer-assisted reasoning; * Links between type theory and functional programming; * Formalizing mathematics using type theory. IMPORTANT DATES * Abstract submission: 4 November 2019 * Paper submission: 11 November 2019 * Author notification: 25 March 2020 DETAILS * Papers have to be formatted with LIPIcs style (currently lipics-v2019.cls) and adhere to the style requirements of LIPIcs: http://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/ * The upper limit for the length of submissions is 20 pages * Papers have to be submitted in pdf through EasyChair: https://easychair.org/conferences/?conf=types2019postproc * Authors have the option to attach to their submission a zip or tgz file containing code (formalized proofs or programs), but reviewers are not obliged to take the attachments into account and they will not be published. * In case of questions, e.g. on the page limit, contact one of the editors. EDITORS Marc Bezem, Marc.Bezem@uib.no, University of Bergen, Norway Assia Mahboubi, assia.mahboubi@inria.fr, Inria -- Vrije Universiteit Amsterdam _______________________________________________ Eutypes mailing list Eutypes@cs.ru.nl https://mailman.science.ru.nl/mailman/listinfo/eutypes -- 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/7883ba07-5dea-8bcc-673c-5bad76377994%40inria.fr.