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 11892 invoked from network); 16 May 2023 08:00:42 -0000 Received: from mail-lf1-x140.google.com (2a00:1450:4864:20::140) by inbox.vuxu.org with ESMTPUTF8; 16 May 2023 08:00:42 -0000 Received: by mail-lf1-x140.google.com with SMTP id 2adb3069b0e04-4f19bffbc23sf6242447e87.1 for ; Tue, 16 May 2023 01:00:42 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1684224041; cv=pass; d=google.com; s=arc-20160816; b=gJme7qqV2pqj6SgQNSxMOYsEqHTJNOPj8X+to3dA+iHyXaB8c7iaFIZSCKJ7UwkJOU BU15FL7n0f7RGVF3WLYMuh7TP4bS+22Y9+Xxa039cH7fq/5PO5WFVLjm57rUtYgpUONC uPYKU+R+bN8pijSzPBqMuPNdAN+6iyF6L/ujb5E7ArwZ6NAJj8wRIZjZBWce+zGmMSW2 11kTB7yDZ82/kHbQuGIxBPIdPZJmbW5+9/jN3TJYDbBdSCxr4r2QujFucCnpr1oRP4Lf xpOi/wPS7x/6ResMcjyG7WBPK8WmPCNOGbN8TQgbeSjhVPQaZW8hAgLm7S3Yu09d4cI4 KozQ== 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=DRZWbaVBqXKGdmC72O8a1RXS+E8ipUwgQ9tpPpLweQM=; b=mJV30VJVZdUhiiBv2hH3CRcBjbJEoI4/+asPck39SLAGEI7V2Ncg8KxoDqLtWgAwH2 Fcnvk+xxfFjQNfIbBCCljyATi/lBTTrB40N288CAVCr3CsXJ67INnozzVIMa7dJPKqoy kuGiQneqtPWVoOkVtGqGyO+fbhi3swfkoPzlBqUDYmqkw0gQo+GZbOYsSgenXu1ZMzhI CVSDSpx69XtP6m3Y2xfNrujesQJfa8bFsC8tnR/n2x8sKApcDDJezRkKovfiB2C+ZUMV tnlUcCpqxUztJ6Nm3hGZKbmg/6TfsRrV7x1HvJaUonky+mEUrQxeaTFemggg7gK+Falj z+Sg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@inria.fr header.s=dc header.b=Wjej5VNQ; 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=1684224041; x=1686816041; 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=DRZWbaVBqXKGdmC72O8a1RXS+E8ipUwgQ9tpPpLweQM=; b=oCiZMY8eu3X8FXg3PfYdjId3so2rYCqLI+KAHcbOIAHjdXbsnP0swl+r+VbE9a/JkZ xVzpYRkZXFInLNXqhr6V++rObunHMk3NFLN976hoJ9hITfRJ8DhuzA3EuHFhjtXl+7gV aKqf/unUUwggS/e2LQ6SlNbDywSJiSyk3Iqayh77xss30r5iFvmI9L0z2mlXyrFi6gO3 sY/WPhFu3l6LPyz4eyHzwCWeWq5Yj20Dzl3DMguJ27EF/3kApMxn2mkcIrOTNvZnA6JZ KE++7fKikPOcisCt1uIzjdrFihzcKeJv4xLh1qujrmjNSP2y5rbHaLUqCB166Jq5sAM9 xQqg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1684224041; x=1686816041; 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=DRZWbaVBqXKGdmC72O8a1RXS+E8ipUwgQ9tpPpLweQM=; b=XddbdRukWEFkKv/in8mF8INTMOrcvpqEo/kTztBe7tvuEp1nNld6fxcSKJLy7u3K8u c8veDlx/TtClhWdMvc5+bw+aH//uM8aoTIUqBEZk5EjrTBwDqBtngFYMCcfKFN+YzRTP X/IKIkp8+y7kHqmRKs9aGOXLIqpSf8UDU5WiaCy8Z2dwtm2M6skNtfVpOMt4231985Hv O3wuqutSipZ3r2ZErm8vR3QuwGGpK3tOocwjt/koUmiIWqHdBPlCYgZA6iYK8maKNfaQ wDgueOB7WNLqteAirhejjGYLsFKL/b2cP8tlARgZmFNXdBYkN/7f3UCJzRqEx6WeyLpP 9zww== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AC+VfDzJsNbRI35OsfJoA/JEeA+6r5zKLhP/UgGicbwxd6XNJaiaxgbn KPOKU9BA1u/r8m+wiRRkf30= X-Google-Smtp-Source: ACHHUZ5fO17YRMAaDZdDdFe86pRlyXCo3bkLdCISLtWuKFSR3P1tK6wE66o68PgZDcc39gXiHPm06w== X-Received: by 2002:ac2:4a7a:0:b0:4ef:ec92:5aa1 with SMTP id q26-20020ac24a7a000000b004efec925aa1mr5863008lfp.12.1684224041386; Tue, 16 May 2023 01:00:41 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:bea9:0:b0:2ab:4d:c40d with SMTP id a41-20020a2ebea9000000b002ab004dc40dls2041686ljr.1.-pod-prod-00-eu; Tue, 16 May 2023 01:00:38 -0700 (PDT) X-Received: by 2002:ac2:59cc:0:b0:4f0:13e3:a291 with SMTP id x12-20020ac259cc000000b004f013e3a291mr6514373lfn.28.1684224038771; Tue, 16 May 2023 01:00:38 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1684224038; cv=none; d=google.com; s=arc-20160816; b=z+nh37CXyRG6Jpyd/yL5FcWo+0OoTPV/QJRWK9Cx3UNB0Iae4iPJ563CegwRRdOxmH UKhZL+ybOZ57bIKyWEO48UqsLNUWKnG+7zxw9dk5/zmDSZeznta/e4aCOZCanwbekexs Q3YkLZOQUjD0x6dJcHLLTxRRhGp9W3cNT9+S2onWyrMYc0Wz0bwR21Ah5+cUH/DC+sYj HMxE7Q0oWK4ZUVeWfT48QrwEJkJuCUJH/0bdZ40Fdr0tVr6XQz5EoWH93qHU7c1Dk5fw Q3lyTqLoEQo1GRuIqqx16N3AppQUL+a6HT2XG7MZrsgBnGIttL95GVl+uJnOn2jliiKz RAKA== 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=Z7G/jbMUdJHYKzJjyE8/PFSKyZn4RY/uP4LidxYHPq66xSxD6FKs2G6l+2r6bDcjNT 1lXVFPhSkCf1RCjQNz6dI1XjrYh7v2hWHlsZs1uDEyIswSQaYdIn5Z51CYECbw+F1IZk BnbVq1EQLMILvwpos9BZF5sGo5esujmGgOhA5zfdA+m1FbsahuxbAN9BOzuvX0iLpfHb 62KbhZ2sIgJ82LNk8pKgSoHhm7IDlVM1xWRXC/QhrtguL+bFtFv5BHGaEgdHbwdcSt1A TNFMhVbBwggMi9+0r7Cr8Qki9hdfx59qlZPH8Tu6MOs9EMpCGCmNUrRdCcWbwzGFHN0w /5Jw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@inria.fr header.s=dc header.b=Wjej5VNQ; 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 u8-20020a056512128800b004f247ec2efesi1248199lfs.5.2023.05.16.01.00.38 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Tue, 16 May 2023 01:00:38 -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,278,1677538800"; d="scan'208";a="56178889" 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; 16 May 2023 10:00:38 +0200 Message-ID: Date: Tue, 16 May 2023 10:00:37 +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] 2nd Call for presentations: 2023 Coq workshop 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=Wjej5VNQ; 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/d1fdd57b-4f35-2919-6676-29d77af7e35d%40inria.fr.