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-x53d.google.com (mail-ed1-x53d.google.com [IPv6:2a00:1450:4864:20::53d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8ae7be5c for ; Wed, 13 Nov 2019 09:28:37 +0000 (UTC) Received: by mail-ed1-x53d.google.com with SMTP id c11sf1066063edv.23 for ; Wed, 13 Nov 2019 01:28:37 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1573637316; cv=pass; d=google.com; s=arc-20160816; b=yh4qIm4ZpNarbu27zESbQDxSJI5Ftw7pT/CulUAcv697cRNuXsKKc8Bbeq7TkVPLnP b80nCvd9KMDUlzajQjrllJTkiII4eDEnNIWINXYAtqLKZEvZM5WOAOVs58JPx2Q/glhN Ysg4fEzxQfGF1mHTCia0Jhd5qlCVwk/xUWzyE9HhWQVDQJE3I7Iuxy2VM4S4WUmZcTnN 7KmtkWQCiwKMdYQdx3JVNiI9dyy1+EOvMBNLnji9WS6FCiO4M/m1JcKsgtJThXSIw5x2 XiAvNn/6hBc15AhYhBbQLnllt7UMJmg51d3sUTOTY+EtOr6Qr8k1lWIkOU8Kgpq+JcRA sk8Q== 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:subject:to:autocrypt:openpgp:from:sender :dkim-signature; bh=TQdNVLvHneWP+VV9i/8x10UxzPAerZu1CQG3K3KG5MI=; b=eYNZN5+aK6ucsHuy/7uGUbngzbmAb0SiXISYav5Q3fKo4nbO8e/kcZoGGIwUi+UdPK MUccqR5dP0slIjSzeN/dMN34/HDZAUjzq1+Qo4DIek5rfuFtTbMsN31NZow1b5z32beQ 8VqaMRKONQ6x62RCexEJX3NIPrSDz2OAApgaLKWv3bhFi1LgfI/WlMvm8r/RmssTfueh m3Y6ppv5oKwxXDrxJDx0PylaTAq4LXkUEd8niQxnEihaS9H/UneBMZApw9CEkkxNJA5W eWpzdHt4OsmqB8M70FYUCoolAkMRNk9qNxVxBQWf689qe8MWslwJRGqsXIhOdEFwQych nKLQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of assia.mahboubi@inria.fr designates 192.134.164.104 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:openpgp:autocrypt:to:subject: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=TQdNVLvHneWP+VV9i/8x10UxzPAerZu1CQG3K3KG5MI=; b=bxCBcO59zQwalWFnQXMvI8uC8jMfK52dUDeEjDairYRXj4xTd0G/+L3+f4dg+xiL8K SqiTDo5I6adYAY14/8iDwR2pdhDjKWsiokZk0xmkoNacEa5WlnGz6OFj3dQVoeXQMTrV Y9af0WfWtj3GBHrdtY1jZifVRFGNVLqjM6V+Quu9PAaFx+7oHaorIXUiDeopXnHs+Tku Rc1dQYulIjbW3xnu3XeikC7/tXJzcrbDPUON/S7Xdk3q2NlPYUcqPzQDH0T+Ye6Waxbf +F3pVfwKtn1/gNqQMnirE7utQRqfDJZB6WyXwkTJ4+sFcpBB65WOTmeDJY8JMVflM0KG 8Jfg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:openpgp:autocrypt:to:subject :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=TQdNVLvHneWP+VV9i/8x10UxzPAerZu1CQG3K3KG5MI=; b=Dnxxve1wSQuK8gbdZQWz8XhpCcOdUf+Lw5wIviGWbQx2Ql44Ry0jRP2+QKL3cELyPM 76g21JsnibC5H0/5PSWIZz4Ofnw9tiywkT42tVoDznaVg1UXir6VQoyjNQM9Q1lRVnMk AlsEdTAQ4XMv8AUyt+KbO1YsIqS8Ms29Ru5wPH8G3T7IIbSsMihjJ90EU7EExkLiylKM nI5Xgw/c4Qz4hX7f1IP8dpCBqlwKKe2iqVysBb5xPLu4zWR79UvhGOXBFw8M30ku3Iet WGNjEADOY5/VOq8goWQcA2RFDva0dEmGXTqsjIbZnllXnNbhvuKzwRY1vLzxPeEpl7TI vJuQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWrQ5fehDAhGz0ff1UtHHn0DKujcmO7oh/46m7W7mk3qPkUIT0F l+FBmFrcE02oQ+wXOHJ9QzI= X-Google-Smtp-Source: APXvYqz2seRQnEkaB4azKKNdJeb80cbnjksC0kIsaBKVP9dK6EzxftV5NzZWVcsV9Ja9ja4YG8mz+w== X-Received: by 2002:a17:906:394c:: with SMTP id g12mr1703413eje.233.1573637316360; Wed, 13 Nov 2019 01:28:36 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:fc87:: with SMTP id f7ls477932edq.4.gmail; Wed, 13 Nov 2019 01:28:35 -0800 (PST) X-Received: by 2002:a50:d80c:: with SMTP id o12mr2387630edj.251.1573637315859; Wed, 13 Nov 2019 01:28:35 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1573637315; cv=none; d=google.com; s=arc-20160816; b=QMSEjkt6gNU/j480gyfWEXGfh7ueaKaSrXFNdzuDvqcfLmcmnETPo6Evey7/vzcdrO KcgBTfY2m8mIAgD+k3ATql0QvgXfIdw64cw6FhLidxqi23mHLOVR0Z4g+cePhx21gESE USa9Tl3NlCNqVoXLbHwNwtsYI6xrxFDzT6kIYIjsD+J5W+4Gev63v2fbCQy/QN+wpv7S qu0URcVV7ObJrGMicwnHDebFBCDv2dgbXsR0GIc5LWM3B/TsVB8Fd+nuKVr20z9ZeQSY zmhuUt7YFOEaLoIJrwARYxw8fBAVeq7yYGG0BGReFIXZ52GMJyh1F0BIkw/4wl77s0VZ lRhg== 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:to:autocrypt:openpgp:from; bh=BRWXvT/ckA1Q8zpZ4JHlqgfip9XbmxcV0wxxD3QUc4M=; b=MQnIdW7SpMYSIm83bR3WNuMG5TjhYgECp2PljNNCs7jDHtkQ1sAIdUqerFWbBsBJp4 hkyVujgrxwXlOsltJhn6jIL39puYJA0nV1IKkl9tve/IP1j0gts4xaeGF0Fb3TU6AWKn kqrFjP+45FVBKq1Mz33JEAnd3JPdug7IZaP7M0+2e5NecTl4V+u8F1GZDrmGIblzp6TH JJi0h81hFPVSAZagoGDd6+oGqSwTdCtqGS0MQDX5r/U7WHnpHgQGPxCWgCNaeeL/YMJc CKVTZbe1wRUhRFM2TBeCfDZqkw6DSz9+3HUQUnFsK5ojSwC5olFlvJtI6aZOHy6dpZo0 si5g== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of assia.mahboubi@inria.fr designates 192.134.164.104 as permitted sender) smtp.mailfrom=assia.mahboubi@inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr. [192.134.164.104]) by gmr-mx.google.com with ESMTPS id l37si130343edc.2.2019.11.13.01.28.35 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 13 Nov 2019 01:28:35 -0800 (PST) Received-SPF: pass (google.com: domain of assia.mahboubi@inria.fr designates 192.134.164.104 as permitted sender) client-ip=192.134.164.104; X-IronPort-AV: E=Sophos;i="5.68,300,1569276000"; d="scan'208";a="326533622" Received: from unknown (HELO [172.28.33.39]) ([193.52.83.10]) by mail3-relais-sop.national.inria.fr with ESMTP/TLS/AES128-SHA; 13 Nov 2019 10:28:35 +0100 From: Assia Mahboubi 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== To: "HomotopyTypeTheory@googlegroups.com >> Homotopy Type Theory" Subject: [HoTT] Final CfP: TYPES 2019 post-proceedings, deadline 24.11 Message-ID: <1b5ff232-a710-36c0-b891-733c84902a32@inria.fr> Date: Wed, 13 Nov 2019 10:28:35 +0100 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.104 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: , After several requests, we extend the deadline to 24 November 2019, and we welcome new submissions, which missed the previous abstract deadline. 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 * Paper submission: 24 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 -- 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/1b5ff232-a710-36c0-b891-733c84902a32%40inria.fr.