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.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-oi1-x23e.google.com (mail-oi1-x23e.google.com [2607:f8b0:4864:20::23e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b38108e6 for ; Tue, 11 Feb 2020 23:03:33 +0000 (UTC) Received: by mail-oi1-x23e.google.com with SMTP id a74sf6869450oib.2 for ; Tue, 11 Feb 2020 15:03:33 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1581462212; cv=pass; d=google.com; s=arc-20160816; b=f84oXy+sIuCSq+Q2IRFml/zfrZlVSMCdgj/8TTaH/wriyCdKQhsAVs92NNuSgx2DUF pOdSBbZ0L5bqRNu0bwk/9qT0jhles35Vo5VaSd5cnxjHBWa2BW8WxS1CVzvYvopNP4Q3 nkRZzMYKGBYmlXJKU/+Y2mPw8+CVkuwcF+C8pryKV8xmyOT8QXZEiFoG62X9ZnHF0GOY Qv+EItpGt5c8V0etqMwzPLKz8b9T2LFbVhDW67fNaCGrnga9SgJdUHO5EaZYEfe7ArOz fuo/iB0hKFaZUdzky53Mn5RL1sNKclq3bwpYrVMgKgJipZigirAquj6TsjtWK/5nfZiN JTCw== 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:to:subject :message-id:date:from:mime-version:sender:dkim-signature :dkim-signature; bh=s1ge288rDVchXH8g2nd1WyQp3pPd0A50QP1mwJs2iR8=; b=ZVwKiO+lyyIemL5xNYB7KF0A/wEs2kujCnAbtgCD7oiwgvbeo9zY8n+YeOhn4n7cw6 18jLatpooqcEEo8KtiB2GdfN1HteCt9Wx1yO6Ak0ejtv+UTBlbOLdw1PbJsxIq/NozpC Kw22stVq8NngFYlqCkibrVwyJ7fc9TJMqtDIXuqkxmMZhz7KA8GNdrEvS4hfMXxd18cJ 2tSRz7+2ZhtjvBR9MRH9ktlHIa+Gc0vlYywUwcVCCKAR3muf33q8JFDpvaBDLqLtDRHR 0GIw90ER1Au7RoJmacAQq68P9vEMtJPEDPjMupOHZsCPZq8ZHdQJnjN253Dj5o530Fa3 50kQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=t+d8EVeQ; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::236 as permitted sender) smtp.mailfrom=andersmortberg@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 :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=s1ge288rDVchXH8g2nd1WyQp3pPd0A50QP1mwJs2iR8=; b=D2NA5GEWn83KIsz/3Bk9MUeXGhUlFq3fbn3+R5RhTkviPWeLBnU5vBKbUQkbYjuFa2 Ihhbbu0LzHlN5uKU9rEFSq/ohYF3K2h53vaKLWQ5uFcXO8V2g0ARbGhtKluy7oAeQvjE S92VgPJeSleUHE85aQFe5XmjMGbSYV7FMaihENJpBPgJjnLBcUPKngrisUJDUnmkITY9 hCXBb60uP1A4quKDT90I1Hburq9//afjtsTsxSRPrzvwnIZdfw4vhKuARNZR+I5J9u3k zV7VJdyYY3Od31nLfAnU1ekcl6EoxHLcZsX1W5yNMwi4q36Upepi6rY2O11K6ZpKCmtQ I2pA== 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:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=s1ge288rDVchXH8g2nd1WyQp3pPd0A50QP1mwJs2iR8=; b=bU4RlVf/zvS9tYR8TZ11+xyBPLQTsZ60Lhxnj03ZKNwjeU9AoAh9EMBNAZwm+rVNpn uiA+Tgvgi3aQioCtahcopscm224/Ys1hMgynLCHFviONF7JYkNwoCsFhR1/J8FOKjN/6 RJRwu46Pcx96TQBc4GgwmSHaY1wGiWM3b1T93sYaweTmtvSv5l1CpzyrvjAQD/LwQQAA FCChRZwB2zFKqIaL62PbLBVRQrBKc9zUAMKXMY3Be2mRvYnwgil2l+gnO0ogOlFUbI2B 6fLz1wiSCoArnA5oqVNKiuamu3DMWotkMtTFolvPTKr6qczGkCk5NwsUU6bod9ajXvwh 7jnA== 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: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=s1ge288rDVchXH8g2nd1WyQp3pPd0A50QP1mwJs2iR8=; b=E1VwMLn5BCoRfotOkiBDlzB2/9K+Vt40Fd+FmK19PwIVuOuW8fkQtTHTU3jSHt8ATi p31QeYDgS6u5LagTvXDww+mCxjVqhWWMG2Gj+pto0RKravt50vFZhk8myr1eVJH9X0wY 5erHNVgCXV37NiZgt7STyVckN1mH0Zy4ojiFQ7T6PQe4FSPhKtuYH46oYQueu0b1Yvbj CgUhSqaN4N89P6h+4tACOroS6GE0REczkqaqDJMJpviblr60Ag8yYQyLiDpGOOBXO53f /+T0JwUn0IjAKeK0etwD7ubvoKjVbNAs8WR6ULIsyZ4XD9QcFfjAbM13rbaaNvMVBFTV L10Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUkQpm/fWUcR7mgJMkSw9/E7Yq3LfFGpNJzYD8Hv6qQenKjpeVW wwCNae8JoBNI4bax8/lXLj0= X-Google-Smtp-Source: APXvYqzgqdCJd3QGpYUe/cT36pGhwgi9W9q6JHKXBXuIpxgac6k4Y8R3kxOQ7DnJ8p3eTCeSRPZp2w== X-Received: by 2002:aca:c1c2:: with SMTP id r185mr4518965oif.19.1581462211599; Tue, 11 Feb 2020 15:03:31 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:7999:: with SMTP id h25ls3903571otm.2.gmail; Tue, 11 Feb 2020 15:03:31 -0800 (PST) X-Received: by 2002:a9d:5784:: with SMTP id q4mr7272596oth.278.1581462211170; Tue, 11 Feb 2020 15:03:31 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1581462211; cv=none; d=google.com; s=arc-20160816; b=TPKylgzijDJ65WSwFXrQ5/s784vpF6B5banRDqakiBO8Mw9HXKjpezZ5f+nyVSP3f9 WW/+/AfCcaeJ2hy0WyqZOVNxYqORGNnTbWzbWGuNH9UuMEDWQ7M8fZB5INe7MCmzpnKh jeyYrAxxoUF1AYrhX4FqFds7pkz7eBw7oWyKtZlvd+nuwFfj06tkakLuQU6XOkvA42ou hJTUEG2444t7E9vxSSDZsM65TpjUf0/E/Zhl/IMoZl0GVUEe7+Eddg3cbzpIvQInIbqT E29qZajkFx6mxqJ7PDRQsKr/uUYVF0BU4IY2N/l7D66paCVu/RCXYzOUk1UAaTlR+Smd AaCA== 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; bh=CrQshvL1ExD/BqQoytSpvTlNKj7rrIiUHP8UCwUIMbk=; b=n+q6KjhEakWDbASvbeFb1nWMxPtNKCaxCRc730EtEwLjefm2V0tXIZlSFodXG13uOO 2zWyA+1N7iDmHZ8mLrzQEmBvDKUuxxIGUjE3yzG/NHafwn+u21KnYZjzj3uK0ycV+GLZ r4xJ6Ad9BjBmmMahf80+K2V4JAdH6v5jhq+WIZUQu6Sogh0GIEjP420forPMUql3iZaA mmIaYP5khx2tMNDcBXB3PFPX8EGf/B3/7BtapFSS1lDgvZpik1FmER8eigu66NSED1/6 QaJAZROM3bY6scA3X4uqS91lsEf0ZWTTkSxhyQFWTuEWLWBkg+YDSJRB+KCR4PW+bGq1 AUHw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=t+d8EVeQ; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::236 as permitted sender) smtp.mailfrom=andersmortberg@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-oi1-x236.google.com (mail-oi1-x236.google.com. [2607:f8b0:4864:20::236]) by gmr-mx.google.com with ESMTPS id c193si295151oig.2.2020.02.11.15.03.31 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 11 Feb 2020 15:03:31 -0800 (PST) Received-SPF: pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::236 as permitted sender) client-ip=2607:f8b0:4864:20::236; Received: by mail-oi1-x236.google.com with SMTP id d62so119478oia.11 for ; Tue, 11 Feb 2020 15:03:31 -0800 (PST) X-Received: by 2002:aca:d544:: with SMTP id m65mr4427855oig.177.1581462210674; Tue, 11 Feb 2020 15:03:30 -0800 (PST) MIME-Version: 1.0 From: Anders Mortberg Date: Wed, 12 Feb 2020 00:03:17 +0100 Message-ID: Subject: [HoTT] Call for Contributions: ICMS 2020 Session on "Univalent Mathematics: Theory and Implementation" To: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: andersmortberg@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=t+d8EVeQ; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::236 as permitted sender) smtp.mailfrom=andersmortberg@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: , The International Congress on Mathematical Software 2020 (ICMS 2020) will be held in Braunschweig, Germany on July 13-16, 2020: http://www.iaa.tu-bs.de/AppliedAlgebra/ICMS2020/ICMS2020.html There will be a session on "Univalent Mathematics: Theory and Implementation" at this event: https://univalent-math.github.io/ Title and short abstract submission deadline: February 23, 2020. # Aim and scope of session Homotopy Type Theory/Univalent Foundations (HoTT/UF) is a new type-theoretic foundation for mathematics based on novel connections between dependent type theory and homotopy theory. Recently there has been much interest in the constructive meaning of the univalence axiom, which has led to multiple new cubical proof assistants natively supporting univalence and higher inductive types. These proof assistants allow for the convenient formalization of abstract mathematics, especially synthetic homotopy theory, and also provide several features previously missing from many type-theoretic proof assistants, such as function extensionality and quotients. The goal of this session is to gather experts on HoTT/UF and its implementation to present recent results and discuss future directions, including but not limited to: o Implementation of proof assistants for univalent mathematics o Cubical type theories and their metatheory o Formalization of univalent mathematics # Submissions Most talks at the session will be invited, but there is room for a few contributed talks. If you would like to speak at the session please send us an email with title and a short plain text abstract by February 23, 2020. If accepted, you will have the option to submit an extended abstract (4-8 pages) by March 16, 2020. The accepted extended abstracts will then be published in the Springer Lecture Notes in Computer Science (LNCS) series. # Deadlines * Title and short abstract deadline (strict): February 23, 2020. * Notification: February 24, 2020. * Extended abstract deadline (optional): March 16, 2020. * Notification: April 27, 2020. * Final version of accepted extended abstracts: May 9, 2020. # Session organizers * Carlo Angiuli (Carnegie Mellon University) - cangiuli@cs.cmu.edu * Anders M=C3=B6rtberg (Stockholm University) - anders.mortberg@math.su.se --=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/CAMWCpp%3DT%2Bixw60EvtrHuAqLweARJzdc9HjAQBrw0%2Bx-5kPeSa= w%40mail.gmail.com.