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,HTML_MESSAGE,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 19232 invoked from network); 26 May 2023 15:56:53 -0000 Received: from mail-wr1-x439.google.com (2a00:1450:4864:20::439) by inbox.vuxu.org with ESMTPUTF8; 26 May 2023 15:56:53 -0000 Received: by mail-wr1-x439.google.com with SMTP id ffacd0b85a97d-30ad2eed51bsf501250f8f.1 for ; Fri, 26 May 2023 08:56:53 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1685116611; cv=pass; d=google.com; s=arc-20160816; b=mKO9IdJnnhnDqkFwEO9k/AU4VFxN9RQlGW+sWFt6RLSOs0BdulZe29sddQ8/yrG3MT PTgvEyblFliRjexOHZrWVQvxEYhtdFzzl+5RYCTFDtOspj6tMRbhFQFfg8c+aRIktQYl qMkUPXap0sDJ5plHX4EGHFEINTGjs6F7qYrhaStXYnnSXMdJiFB+H6FfJjIggH8d8KeI S8WoReoDtq/LV7mHcOgRp+mxajU8kzYV/R7PI7uwLPLZGDSln9GeYUHNsYtLVPYB13Xm kMl8vImDIFFkwmCWTve+UEeCx4eunQHQYdsySvxVvx8J5Oi6S79fLdbHPCB3N5b9UpnR 7V0Q== 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:thread-topic:thread-index :mime-version:subject:message-id:to:from:date:sender:dkim-signature; bh=DqUSOMoejbq9eaFtSAIv1PTFOKE9nPojHPHZ9zrsfSc=; b=JnHg34Fo6svt9BHr2OQjTI5KNELkwvn27W8Z/d+kHuIBDgRRp/IVgzrePgyR8vrlZz mtXpO6qEMp8ZzZbG/ZuZ3OFMo/kdXVNtZbtN+l3+BdvhK5TuQGHd+RXE1bPyEKAPJDqU ui4igTRgS/qqzSAqN2v5D556jGsMyPHyzDbtiN5QWt2NJbX4nOUp8eOxEa4yIi0LF0ul 3Eix+3zKayRIh1Bc+7U7WIg8EnKmzjvBz52nFxs9oYuzC4IA7CY5kn/J8tRr0Nz2t6mH C8zzyan38n43z7xppTKPDE1KoJB9Iqt0JgshKwIS/xRt2WRVG9r36S/rfLadRuq9dC+m WgUQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@inria.fr header.s=dc header.b=OQQ2qtmp; spf=pass (google.com: domain of yves.bertot@inria.fr designates 192.134.164.83 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=1685116611; x=1687708611; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:thread-topic:thread-index:mime-version:subject :message-id:to:from:date:sender:from:to:cc:subject:date:message-id :reply-to; bh=DqUSOMoejbq9eaFtSAIv1PTFOKE9nPojHPHZ9zrsfSc=; b=Q3N+5XTEmyyPmbquUj83ZkURNSjbzYdEyQwArUGFkmDcYpTb0MeNvNqQn0fuR1/DPM v6UDOXLpkwt+gzHVIW2nIwhhj4atR4Q8nXV0XXVAY/pR6iCIc3jU30wrnpfhujgBMAkn MHIWtqHbRoj7fnMeNueQdvn8+QXnM7cYq/UXUncq/fOp3uqpukgcrXLpJmcaC0BR8NSO tHRErLCijE+SnbCrqGFFXOgviiM2MisLndsGrVq6zEq7s13N6VkbsVWjwV39x1pcDQ5x 1loC6QnfyWMEJ+sxPEddxRpfZogVpj8XFFyzAOJfNqEc1BP1MdMjjpAt9uqbfwYTf9yD GQTg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1685116611; x=1687708611; 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:thread-topic :thread-index:mime-version:subject:message-id:to:from:date :x-beenthere:x-gm-message-state:sender:from:to:cc:subject:date :message-id:reply-to; bh=DqUSOMoejbq9eaFtSAIv1PTFOKE9nPojHPHZ9zrsfSc=; b=IClI4LblDsJ9sapN/r22rvxdUIfjcKMZXBJXo9aSlhy+glepsJyyfxq/MHHqlmCpyJ xHXvpPKU9053WXo44+JULUZvzbNiw0Lvre0LwKGHnJPyLDhghzXtlW/t02jDKDSYTPbb JIHLDX/fciqh+jfZVIbKCfJ2J7YSrwhxBiK6epszuT5Ejrp4yR7B761h/Zjv7PHZtdID WFqSsmjEfU7oQ6WKB91xFzZbyo7m5KLr99UuFJymdUZ/ZqxkHLBlxolZXD1vpxZnPUqc 1tagqXLg5+PPEmBtKr9sV5kWIq/ZnInK25/2yVjgdkW5R3ClwCGEjPJ/gK45jOAUhdj3 QMpA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AC+VfDwM8DNT2Zs26l16NhrqpBXlVBHHEhKOXk5AUQjniSo+Ldr1unB0 e4QDL+0AD0d0UtuqR5nWhkE= X-Google-Smtp-Source: ACHHUZ4iApsARpgIkq18ITB90g/lu6U3GGj76r95VUivqj1r4yXBRhYHNl5Zy9mAElBgOWUkvzRYeg== X-Received: by 2002:adf:d1ca:0:b0:306:28af:9a1b with SMTP id b10-20020adfd1ca000000b0030628af9a1bmr1707250wrd.1.1685116611196; Fri, 26 May 2023 08:56:51 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6000:3cf:b0:30a:93c0:47ad with SMTP id b15-20020a05600003cf00b0030a93c047adls1427083wrg.1.-pod-prod-04-eu; Fri, 26 May 2023 08:56:48 -0700 (PDT) X-Received: by 2002:a05:6000:196b:b0:306:2aa7:2ed2 with SMTP id da11-20020a056000196b00b003062aa72ed2mr1897648wrb.61.1685116608781; Fri, 26 May 2023 08:56:48 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1685116608; cv=none; d=google.com; s=arc-20160816; b=H4sgqRhi6M5l/3LjL2bndrx0mmJeX1ewAmDKIjmNxoYZJW21yJeZFD9UrJ+9Vx4x5P ybY7AHrnRuriyGISplNhbly2sNNkG1bf2aVF2dDlt7kOhDh4eEVsYQNFoUbFzK0wpXWa DxENA+MEjFEGxzwgMcuyiha6ipGpoo2Rj+z7Dx1MieKR+ES08wgFaXGhAI86n9HjgKU6 mBNIq0xVI6y9WgKNPyuMX3UJkxXeSNOF5HV84O0JcPfwUmi1zuO964RnHQS/sVMnm36l Pms0aDggHfBkLbefiAG7EHVZxps0guUcyfwW+dWxvZZgQhu22nQ9TDqRJ6orw7TO4pxC g63Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=thread-topic:thread-index:mime-version:subject:message-id:to:from :date:dkim-signature; bh=Ghww5eECMBZju9+Ih7HuzK7VnDhteUONXRtHlX/UxiQ=; b=fPTzVoSpy2RaQG/3g5SyaGJeg8CIQ+Rg5BEAYq73Bt0obbsbZB05ZzKD7Nhzg0pOTq d9froeqLd7e5Ijgg8xL0rKlrXhcKqN3B5rZMkvj/Im8Vule65n6VXXisHWrGiA30tIoI O0PXupXPI3kqFVbAOprKxTG3o9wkmI8UXS8B9xoqm4Nnm21XAjNbTwcawswSl2hG5Xuw SiixkegDnX8lD6qy3Y1QBCvK3fVbhR3JD+A99xoT4ZZIefKsMfS/M6/tVchu5vjEpqXu /DsIFG0dAXaUJCaAohq9KsCXzhwkewbhAXMI/ZZqOby0XZiPEez4xGUUJomHz6hCyok+ pOSw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@inria.fr header.s=dc header.b=OQQ2qtmp; spf=pass (google.com: domain of yves.bertot@inria.fr designates 192.134.164.83 as permitted sender) smtp.mailfrom=yves.bertot@inria.fr; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=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 bx12-20020a5d5b0c000000b0030adcfaf029si157618wrb.5.2023.05.26.08.56.48 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Fri, 26 May 2023 08:56:48 -0700 (PDT) Received-SPF: pass (google.com: domain of yves.bertot@inria.fr designates 192.134.164.83 as permitted sender) client-ip=192.134.164.83; Received-SPF: Pass (mail2-relais-roc.national.inria.fr: domain of yves.bertot@inria.fr designates 128.93.142.32 as permitted sender) identity=mailfrom; client-ip=128.93.142.32; receiver=mail2-relais-roc.national.inria.fr; envelope-from="yves.bertot@inria.fr"; x-sender="yves.bertot@inria.fr"; x-conformance=spf_only; x-record-type="v=spf1"; x-record-text="v=spf1 ip4:128.93.142.0/24 ip4:192.134.164.0/24 ip4:128.93.162.160 ip4:89.107.174.7 mx ~all" Received-SPF: None (mail2-relais-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@zcs-store5.inria.fr) identity=helo; client-ip=128.93.142.32; receiver=mail2-relais-roc.national.inria.fr; envelope-from="yves.bertot@inria.fr"; x-sender="postmaster@zcs-store5.inria.fr"; x-conformance=spf_only X-IronPort-AV: E=Sophos;i="6.00,194,1681164000"; d="scan'208,217";a="109929100" X-MGA-submission: =?us-ascii?q?MDG6HtK0b84wWk4suYvQjjb5K3ya1+YFy0wXth?= =?us-ascii?q?XpPbCfEz+4adu4YDGojzw137cCUT/Hy53t0nR8ofFGCYeTWLybQklOM7?= =?us-ascii?q?fRFLQrmSGmDHQ36MiaRHt9fWLUE1/ot9FEaesfY0texwQcVEEns2bmO1?= =?us-ascii?q?YYoQPLY7MwRMWgW8VBdbVnbw=3D=3D?= Received: from zcs-store5.inria.fr ([128.93.142.32]) by mail2-relais-roc.national.inria.fr with ESMTP; 26 May 2023 17:56:48 +0200 Date: Fri, 26 May 2023 17:56:48 +0200 (CEST) From: Yves Bertot To: homotopytypetheory@googlegroups.com Message-ID: <1591065856.32935248.1685116608241.JavaMail.zimbra@inria.fr> Subject: [HoTT] Deadline Extension: CfP 2023 Coq workshop, May 30th MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="=_f0e87f6f-c1c3-4599-af3c-e227ca848147" X-Originating-IP: [37.71.80.102] X-Mailer: Zimbra 8.8.15_GA_4522 (ZimbraWebClient - FF112 (Mac)/8.8.15_GA_4527) Thread-Index: XzA23MtjPpK65L1aGxqdbdHndE48Dw== Thread-Topic: Deadline Extension: CfP 2023 Coq workshop, May 30th 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=OQQ2qtmp; spf=pass (google.com: domain of yves.bertot@inria.fr designates 192.134.164.83 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: , --=_f0e87f6f-c1c3-4599-af3c-e227ca848147 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable IMPORTANT: We are extending the deadline for submission to the=20 Coq workshop to May 30th, AoE (Anywhere on Earth).=20 We are pleased to invite you to submit presentation proposals for the=20 Coq Workshop 2023, which will be held in Bia=C5=82ystok, Poland on July 31 = ,=20 2023, as a satellite to the ITP conference.=20 [ https://coq-workshop.gitlab.io/2023/ | https://coq-workshop.gitlab.io/202= 3/ ]=20 The Coq Workshop 2023 is the 14th installment of the Coq Workshop=20 series. The workshop brings together users, contributors, and=20 developers of the Coq proof assistant.=20 The Coq Workshop focuses on strengthening the Coq community and=20 providing a forum for discussing practical issues, including the=20 future of the Coq software and its associated ecosystem of libraries=20 and tools. Thus, rather than serving as a venue for traditional=20 research papers, the workshop is organized around informal=20 presentations and discussions, supplemented with invited talks.=20 Important dates:=20 May 30 , 2023 (AoE): Deadline for submission of presentation proposals=20 June 15 , 2023: Notification to authors=20 July 31 , 2023: Workshop=20 Submission instructions:=20 Authors should submit presentation proposals as extended abstracts=20 through EasyChair.=20 Relevant subject matter includes but is not limited to:=20 Language or tactic features for Coq=20 Theory and implementation of the Calculus of Inductive Constructions=20 Applications of Coq and experience reports on Coq use in education and=20 industry=20 Tools and platforms built on Coq=20 Plugins and libraries for Coq=20 Interfacing with Coq=20 Formalization tricks and Coq pearls=20 Submission format:=20 Presentation proposals should be no more than 2 pages in length=20 including bibliographic references, and should use the EasyChair style=20 with the fullpage package. All submissions must be in PDF format.=20 Program committee:=20 Nada Amin (Harvard)=20 Jesper Bengtson (IT-University of Copenhagen)=20 Yves Bertot (Inria) [chair]=20 Ana Borges (University of Barcelona)=20 Chantal Keller (LMF, Universit=C3=A9 Paris-Saclay)=20 Pierre Roux (ONERA, Toulouse)=20 Takafumi Saikawa (Nagoya University)=20 Enrico Tassi (Inria) [chair]=20 Organizers and contact:=20 Enrico Tassi and Yves Bertot ( coq2023@easychair.org )=20 --=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/1591065856.32935248.1685116608241.JavaMail.zimbra%40inri= a.fr. --=_f0e87f6f-c1c3-4599-af3c-e227ca848147 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
IMPORTANT: We are extending the d= eadline for submission to the
Coq workshop to May 30th, AoE (Anyw= here on Earth).

We are pleased to invite you to su= bmit presentation proposals for the
Coq Workshop 2023, which will be hel= d 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, contrib= utors, and
developers of the Coq proof assistant.

The Coq Worksho= p focuses on strengthening the Coq community and
providing a forum for d= iscussing practical issues, including the
future of the Coq software and= its associated ecosystem of libraries
and tools. Thus, rather than serv= ing as a venue for traditional
research papers, the workshop is organize= d around informal
presentations and discussions, supplemented with invit= ed talks.

Important dates:

     M= ay 30, 2023 (AoE): Deadline for submission of presentation pr= oposals
     June 15, 2023: No= tification to authors
     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:

 =     Language or tactic features for Coq
   = ;  Theory and implementation of the Calculus of Inductive Construction= s
     Applications of Coq and experience reports on= Coq use in education and
       &nbs= p;  industry
     Tools and platforms built on = Coq
     Plugins and libraries for Coq
 &nbs= p;   Interfacing with Coq
     Formalizati= on tricks and Coq pearls

Submission format:

Presentation prop= osals should be no more than 2 pages in length
including bibliographic r= eferences, and should use the EasyChair style
with the fullpage package.= All submissions must be in PDF format.

Program committee:

&n= bsp;    Nada Amin (Harvard)
     Jesp= er Bengtson (IT-University of Copenhagen)
     Yves = Bertot (Inria) [chair]
     Ana Borges (University o= f Barcelona)
     Chantal Keller (LMF, Universit=C3= =A9 Paris-Saclay)
     Pierre Roux (ONERA, Toulouse)=
     Takafumi Saikawa (Nagoya University)
 =     Enrico Tassi (Inria) [chair]

Organizers and conta= ct:

Enrico Tassi and Yves Bertot (coq2023@easychai= r.org)

--
You received this message because you are subscribed to the Google Groups &= quot;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.goog= le.com/d/msgid/HomotopyTypeTheory/1591065856.32935248.1685116608241.JavaMai= l.zimbra%40inria.fr.
--=_f0e87f6f-c1c3-4599-af3c-e227ca848147--