From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 18997 invoked from network); 25 Apr 2023 07:03:17 -0000 Received: from mail-lf1-x13b.google.com (2a00:1450:4864:20::13b) by inbox.vuxu.org with ESMTPUTF8; 25 Apr 2023 07:03:17 -0000 Received: by mail-lf1-x13b.google.com with SMTP id 2adb3069b0e04-4edd253ba8bsf2554670e87.2 for ; Tue, 25 Apr 2023 00:03:17 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1682406196; cv=pass; d=google.com; s=arc-20160816; b=MiEEmM9QXPL+QSHLv5KpoVA1xIUvJrCVUJ2JvLRievPRs8kiSC+gkkbPq433d68Szv tW/ec5FkNWf7lns2OMqWMbUfkrxBYSw0Jjy0k/xITGiI5K3OiDS0nChvcvfIf8WO75lU dOKYurwbBGRLf1DwsP7i9EvhbKQ7UQMfFWRM44oX7s/z+5kgAuNq6b5G5DABaKSY7BLH niXXrEvqxMC41miVPcHpY/obj6zkgjEcliX6wOuLQg6jtEtWcQ2DGwWbR2bPi2bgBuIe BTgHbPkf8QE9hIUIHpjcWU8PKQkfPIbFO0sgTsoACl3x2vhF38nkrdxqCJSbKfYhDS8m 7Igg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:content-transfer-encoding:subject :from:to:content-language:user-agent:mime-version:date:message-id :sender:dkim-signature; bh=WfaE6bB36Q/12i3vy4//tkkLJItllaiOxt/KoKyiIYQ=; b=IslAvNoEbGkhQ8hYHYaO4jO8Rdb6PhnmovDclN5xQvBsoHcHGvgOXGZmT/zVNxWRk4 YWqfBaPmc6ngi2YuqqO0dwWMJ98bZlF2NyxQxW2Rxvz+9p8F01HRkEaxZLYKFKKPxPv8 XgEw8D4suSftGOcwksHWDcSUTtVVj69TICkAUbNS7R8/lNI8tjtnl+l3mLTBLG5RQo9Q DihpeRjjEPGRYcOjqDCR3kOb67l6NpZEnrTpUPuChoin+d+kxHGJgrFb5ohqExkQdH07 8BegNAGP+zPthHsdoHcu/tMEU1jQKiqBOfX9FwUFS9h+r6UD3tVduv3IewXl6cKcN6B3 nvIA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@inria.fr header.s=dc header.b=CFAhxzwS; spf=pass (google.com: domain of yves.bertot@inria.fr designates 192.134.164.104 as permitted sender) smtp.mailfrom=yves.bertot@inria.fr; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=inria.fr DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1682406196; x=1684998196; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:content-transfer-encoding:subject:from:to :content-language:user-agent:mime-version:date:message-id:sender :from:to:cc:subject:date:message-id:reply-to; bh=WfaE6bB36Q/12i3vy4//tkkLJItllaiOxt/KoKyiIYQ=; b=iDZA4+AM1XytoAnHyDyrLlhuA4dUWgtFGkS/QvTpf0J45UFK86GUfEjNbxtSti36n8 p6EKZZY/cKihZ7sBfL0coi3zsvTX7Fby8oXXCXkR3qYVeWyHn3qmjDyFWwqYDU8b8Sh9 tEPCDoWZp+ap4qk7xI/WsOn80yWsH2JaYaza3SK3Pm54ZW/Rlc/T8nhBjIafUjSIMPvf oF6hZ5B5IIIXjAR52ZD/tUvF0oXMXYnB8K+EWw5QSlKPfZxybkjg1EUgjIGzLDid/InW SkrEVsuyC0xY80Pu+jai5yYypI6sIY8RJrv/OumQm2T8GzxqB5V0loatuhkOEdDepdWA fikQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1682406196; x=1684998196; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender :content-transfer-encoding:subject:from:to:content-language :user-agent:mime-version:date:message-id:x-beenthere :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=WfaE6bB36Q/12i3vy4//tkkLJItllaiOxt/KoKyiIYQ=; b=RWAAvFpykMtFm5SOWG7ccnNQ88qCEFyaOuJKbRwwFTCTw2mB+DUd0k4cPmUsEotV5K u99pzzTOtwcaZjDolBHFJU5Ronjxp5nc70v6POvFQZgDspbR+pbE49PDY0x/iUKcgiNt nK2jzVXklqB1CvkuQy7ULMHDsbhLL6cOhNmfIk26QdabGVCizYMYNFljvW1qE6gcxnCm ybzoYRvlAHUUEm9Vw6hx2kzxYeQFwYDvMeKYbqRFXnc9MjY+G+5aJJKRN63egugCrD+Z 13Gi4JHdq14b3Yt3y6z5lUbDHrRUuqMMROfbhD/9NOfUcn2atoLTCzIekepV2jusaDRO XfIw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AAQBX9fDu5C72sFJeQfyaZwweWI6oVSEgJz5W/3n41nsUt91l6aN7jdU GWJC/cmt6mjtpJphs5Kq8q8= X-Google-Smtp-Source: AKy350ZSwXcqlendga8053KD7dpX98zU1+ft2Q/EA+0N4PxCUgztjXXa9V52SmXJo8W5E9IQuXjasA== X-Received: by 2002:a19:c507:0:b0:4e8:46a1:21a7 with SMTP id w7-20020a19c507000000b004e846a121a7mr3682046lfe.6.1682406196239; Tue, 25 Apr 2023 00:03:16 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6512:4013:b0:4ec:6fe6:9f26 with SMTP id br19-20020a056512401300b004ec6fe69f26ls309332lfb.0.-pod-prod-gmail; Tue, 25 Apr 2023 00:03:13 -0700 (PDT) X-Received: by 2002:a19:750a:0:b0:4ef:f0ce:3aea with SMTP id y10-20020a19750a000000b004eff0ce3aeamr1505811lfe.53.1682406193807; Tue, 25 Apr 2023 00:03:13 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1682406193; cv=none; d=google.com; s=arc-20160816; b=ezwBYSH0Sz9qPi7J7SIWo7ToHdUYI1BDh6KbZ58H5p5MJpSncnEP9YMuYmrRLlWXGP MWbW7JtwOKakd65Vghgkm27yyF9iAwD7LGa1ygnty+JlaDcOWAuFpOaeUKWPawzWDclS qqov6kK5RC2UnTKM4ph35skk8y4DX7/PPMi4ZaM+Cm5RCtRyY6rd1iI8aFWhTxHGSaNs ECh+slXpAi0qKgHtYqkvEELwDjw8pQWCSlcoUoKAeM1Dss1csizQs0l/0Py8KauaZHp3 DtJFptzIUTQZZ7N3muJ0YVZdf+EMtbYjZBa27+pcbnaITwTOB1l4BcLe4QSab2CTo8tH K+ZQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:subject:from:to:content-language :user-agent:mime-version:date:message-id:dkim-signature; bh=ZK6GaJ6fORFGAycVeOzgtBVwFp1NqZUPibVKCfZ0D+U=; b=jAXg0xWLkBapxZMnczgGfZwYs6sdTUQf1KsPmiJ06fL4P+zDnEWNfYP+iiarlmGOXg 7kqqO+8L2i9cMeTuyS45Z10DYGRRVNO46hp7mQHvR/bjWqDuA3pTmyxkhz0WZChi2R5o qvGaMSlZHyFZG1fHXZ+AePqWClA3xR+AX/8VLnK70Bwj7XONRvL8D6w2qF0ECjhmFkQm lu9ZhJNlc1vOhaTKPbuZhAHheJvUqpAwpGES3hOIqqD6O7ne+DtPnEBXNjizz95iX/46 CeOy027npwpxdVCEuZCbrbdJMNb4UzRqC8drt6tyIXxI+B/PF8Ria6lB4lTv96AYFT+/ n8wg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@inria.fr header.s=dc header.b=CFAhxzwS; spf=pass (google.com: domain of yves.bertot@inria.fr designates 192.134.164.104 as permitted sender) smtp.mailfrom=yves.bertot@inria.fr; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=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 f43-20020a0565123b2b00b004ec6206f60esi835330lfv.9.2023.04.25.00.03.13 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Tue, 25 Apr 2023 00:03:13 -0700 (PDT) Received-SPF: pass (google.com: domain of yves.bertot@inria.fr designates 192.134.164.104 as permitted sender) client-ip=192.134.164.104; X-IronPort-AV: E=Sophos;i="5.99,224,1677538800"; d="scan'208";a="54275561" Received: from chet2.inria.fr (HELO [138.96.205.228]) ([138.96.205.228]) by mail3-relais-sop.national.inria.fr with ESMTP/TLS/ECDHE-RSA-AES256-GCM-SHA384; 25 Apr 2023 09:03:14 +0200 Message-ID: <3182c679-e12e-7cab-b95f-166077cff663@inria.fr> Date: Tue, 25 Apr 2023 09:03:13 +0200 MIME-Version: 1.0 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:102.0) Gecko/20100101 Thunderbird/102.10.0 Content-Language: en-US To: homotopytypetheory@googlegroups.com From: Yves Bertot Subject: [HoTT] 2023 Coq workshop call for presentations Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable X-Original-Sender: Yves.Bertot@inria.fr X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@inria.fr header.s=dc header.b=CFAhxzwS; spf=pass (google.com: domain of yves.bertot@inria.fr designates 192.134.164.104 as permitted sender) smtp.mailfrom=yves.bertot@inria.fr; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=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: , List-Unsubscribe: , We are pleased to invite you to submit presentation proposals for the Coq Workshop 2023, which will be held in Bia=C5=82ystok, Poland on July 31, 2023, as a satellite to the ITP conference. https://coq-workshop.gitlab.io/2023/ The Coq Workshop 2023 is the 14th installment of the Coq Workshop series. The workshop brings together users, contributors, and developers of the Coq proof assistant. The Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, rather than serving as a venue for traditional research papers, the workshop is organized around informal presentations and discussions, supplemented with invited talks. Important dates: =C2=A0=C2=A0=C2=A0 May 26, 2023 (AoE): Deadline for submission of presenta= tion proposals =C2=A0=C2=A0=C2=A0 June 15, 2023: Notification to authors =C2=A0=C2=A0=C2=A0 July 31, 2023: Workshop Submission instructions: Authors should submit presentation proposals as extended abstracts through EasyChair. Relevant subject matter includes but is not limited to: =C2=A0=C2=A0=C2=A0 Language or tactic features for Coq =C2=A0=C2=A0=C2=A0 Theory and implementation of the Calculus of Inductive = Constructions =C2=A0=C2=A0=C2=A0 Applications of Coq and experience reports on Coq use i= n education and =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 industry =C2=A0=C2=A0=C2=A0 Tools and platforms built on Coq =C2=A0=C2=A0=C2=A0 Plugins and libraries for Coq =C2=A0=C2=A0=C2=A0 Interfacing with Coq =C2=A0=C2=A0=C2=A0 Formalization tricks and Coq pearls Submission format: Presentation proposals should be no more than 2 pages in length including bibliographic references, and should use the EasyChair style with the fullpage package. All submissions must be in PDF format. Program committee: =C2=A0=C2=A0=C2=A0 Nada Amin (Harvard) =C2=A0=C2=A0=C2=A0 Jesper Bengtson (IT-University of Copenhagen) =C2=A0=C2=A0=C2=A0 Yves Bertot (Inria) [chair] =C2=A0=C2=A0=C2=A0 Ana Borges (University of Barcelona) =C2=A0=C2=A0=C2=A0 Chantal Keller (LMF, Universit=C3=A9 Paris-Saclay) =C2=A0=C2=A0=C2=A0 Pierre Roux (ONERA, Toulouse) =C2=A0=C2=A0=C2=A0 Takafumi Saikawa (Nagoya University) =C2=A0=C2=A0=C2=A0 Enrico Tassi (Inria) [chair] Organizers and contact: Enrico Tassi and Yves Bertot (coq2023@easychair.org) --=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/3182c679-e12e-7cab-b95f-166077cff663%40inria.fr.