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.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,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 1478 invoked from network); 26 Jun 2022 21:33:35 -0000 Received: from mail-yb1-xb40.google.com (2607:f8b0:4864:20::b40) by inbox.vuxu.org with ESMTPUTF8; 26 Jun 2022 21:33:35 -0000 Received: by mail-yb1-xb40.google.com with SMTP id u131-20020a254789000000b0066c8beed1e2sf3373143yba.16 for ; Sun, 26 Jun 2022 14:33:35 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1656279214; cv=pass; d=google.com; s=arc-20160816; b=kxEMgtRGMzRctgymVuMFuAApuZmgp3RjSn+gtN3v+k2dGHFiPrFsTIqJFoYdVR3YEd W87d97kTmABcMxZuonycZwyRWgFxCcx9tdqW8q7ozyGnaCn5Rls/7LCtfos+KQ9MPcsp IbbDZnDeytIkbGxhIbzz2AB6E/JDCnk7OBHuPGP16013Kd109KIOEsVpc0OyXnNGs39l 2IsQ2/HWqImKa7HRU+Nn2GJAT9pq87arDj0Sy5AKKT7mjC9VfuBDkskC3OOYTDFVFw/U SgEXC1+obT8/2o2QXzhRMqxCTCalLbV/43x5Pq3ZS239vNONT2dKU3XeUll/no/CiWgi 3+ig== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=OgUrIRug1R1Z6QxmWBiLJe0M17GEzEWr1u6D7x2DL/g=; b=UHMLVy0vSwXTTnaUmiXZSXNiQo++VRrvAptNAcCxP2Cm3C+UX5yloee3R6vgNiJUCx n2Y2qpvPDtvHCqHuoTm0g3mvWXg5iDA+7HQo6x1S8A8aQ9fq5H0PTWe3XNl+tgM+AcKy 0muuXbX+8Id2L4vxTg9VrRuKH/inkQBriV0Zq4AEV3UTfBWvzcwcCvcJsPa6N3Yrmv2x SsFqRIiuSDZSfV+s+IDgQrTsVaTvuZRFrEfBpAO27n+x2EQl+gkYKsamnlA+T4Oi9MHF GwYe+A+NO5lUt4ew8HdJ8xn6GkjrmyvDQq4+PxuupZk3TYSkrmUfF7B76Jk0KER2oF6O cRXw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=OqepQozU; spf=pass (google.com: domain of kaposi.ambrus@gmail.com designates 2607:f8b0:4864:20::b34 as permitted sender) smtp.mailfrom=kaposi.ambrus@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=20210112; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-subscribe:list-unsubscribe; bh=OgUrIRug1R1Z6QxmWBiLJe0M17GEzEWr1u6D7x2DL/g=; b=fB/le/5c1EpasKqtiOQuI/K4AqjIU8j9rvpX0CeUl9Y+r2XNWIsmhbJYlsEY8IICy8 mlNqvrzqUL6wbpdSU8UyT+FXOwOrPvsBCCB7BgnR9joVScgXjVY7iaZBNE0RIAwMrrSN LwwBiw/qDtcIIUn2h3D0almf7bGjlu0Vfe5jl2Q8WVB/mM8rTuTgnLytf2nmSb4WI3Uj PiJjpv2APa6+2wWnEeesi/qljDRvXrMm9XSkGF9/rn4JvPkWIFXwgESAD04OdoyCBYW7 2GaUj+wZMSbCGeKU1dqUP9cJQyOTYzHQdpO5F17YwGzftEEDN687BVDsIKajJiBtW3ml ehqg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-subscribe:list-unsubscribe; bh=OgUrIRug1R1Z6QxmWBiLJe0M17GEzEWr1u6D7x2DL/g=; b=WT0/VkYPZHfE418v3v7rMEnBTz7w1M4nHfzxpRCQhdVKZ2bT9DpwccYlI87WeWk1Sq 95ikXUuIhuqA58FksT61p7ad5WFAs0cajaQp1CyzmlXzV7NS9PTXXPanKGiqyVhl/Adb TTiEjpGejfaljFq427Fc3Pdx4T5haRBa0Oicqt6HClQ8LqNLMB3NBkKcK6+GgPQYyvYf 5Fs7w1gGYg2BwuxLqhvX1p0SuTfHwM0qq+RGUxE88VS7M4L6Lj1fTf7eC2Nc3LLo6JU+ zhMZAw/Rnk7t8TSYcPCL9X4ZrNglP+JtHWuH4GGOd4DJDk2iaQYKkuoFDNPRN/7tSPEt 39QQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-subscribe:list-unsubscribe; bh=OgUrIRug1R1Z6QxmWBiLJe0M17GEzEWr1u6D7x2DL/g=; b=Ht6tdELbnq5I/APz7fDWdqRfh+Le0iQHz46O4cLH3kHeRixHB3zzutVOJgVEDh0pd+ OL90pmnYWfDzgzRpKy1/6BEYA7uMJLCPiVv3qlHfJa7vSzvTXfVR15jtIUOS7dWuRfM1 gDTO2/KW6BZ3HvKcKVFi7ZAFuqpfQUYVegqXvJPT74DcLAm3oQNG4WKCkob7t8A9FD8F riHkYRbgOj0iOK0JSKcHWnEYabOVuDke0dq108uqloTRyBO+WYKb/rNy2fCYjFt50ail Lau8rwjLxRLGcqn1EbBMzUR/LtsFGMfMmVfTvE1Cnb6pbG1fr+B2Ko1blCJ09ypkwtm8 Pf8A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJIora82ZmIdOrO9PPfGP50xwKoOMTIMgLT2hkD5hZZRdf1a8Yf4PrbV P5/J5AfMhVQd3U2nAtTo56I= X-Google-Smtp-Source: AGRyM1s0X7N9Nj4HijLIdIQ56pxDp9tE271VlJONcKiKcPYRlfkEJtHKlnbKRt/BiK0HTsNHamN6pg== X-Received: by 2002:a81:498c:0:b0:318:b026:cbe6 with SMTP id w134-20020a81498c000000b00318b026cbe6mr12118773ywa.375.1656279214460; Sun, 26 Jun 2022 14:33:34 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6902:721:b0:64a:b88e:63c8 with SMTP id l1-20020a056902072100b0064ab88e63c8ls18847731ybt.11.gmail; Sun, 26 Jun 2022 14:33:32 -0700 (PDT) X-Received: by 2002:a25:61d8:0:b0:669:af98:a5e8 with SMTP id v207-20020a2561d8000000b00669af98a5e8mr10983903ybb.225.1656279212888; Sun, 26 Jun 2022 14:33:32 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1656279212; cv=none; d=google.com; s=arc-20160816; b=kuZwBOcu+RmvhjIsJY3ujyWipDiO5GAZxHoHYXFcCjuCfcjI4E+n6q9lORsBJ8Hcf9 TODHLJ3BvK11iVBypQ1fhQg0ZeGHqUKnk3sbX6up6re1bPj5UA2Ub43zwvUeZ4yxHBN5 HkZ/bpUmcusCw/Ayz1ouHam+U2WVDti5n0f3xtJ3lC44Cq5fbIEYylRFrpwCee28/ONF zRCF4rmaT+t9woeCEohsAvHN098LkLbEU2J1XNazT7e4s0JLma7ds49Pph4a32QByQ3a BLDIOQL8ImqIXOE0b6kKSEH59XzQX+w2+L+lTVMJAYHdwoXdMZVaWpxSAPnk2xtw6pEw nYwg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=+JHfoa14RlhH8V1eLUOgkXObQc80KTEwHNMhh6B/vEA=; b=PqqkldWnAIq3VuduI4RPIVcfz3dl8Us5JN7ZL/Z/vVqOH8JVhdz4VxFUKy5MakO/An Tv9ruBBQHEBdVxRJ+NZtrnzNmC7kWrdJMfD46d+5ETSjEwJfj+mFYPlOXKgwKHkpEhpJ 2yttkGcscAf9yST2lfRRSqOXEJfYmPbFHh9iE91Bu8xfsVxaxDfNmHicS/1+tn024Vk6 XN1P48dFhB4qhgWz9iFvhhcYwaIqp0cLbaDONSBwApHIZ++hHQy4Hg3dJspWe7Nfon2x Qyq3WITHaf0556u2V2CfNvzog7UKtAcS33/GFBcZdouAZH+9f9MJmKrTd8AcQ+J2VJPx YNew== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=OqepQozU; spf=pass (google.com: domain of kaposi.ambrus@gmail.com designates 2607:f8b0:4864:20::b34 as permitted sender) smtp.mailfrom=kaposi.ambrus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-yb1-xb34.google.com (mail-yb1-xb34.google.com. [2607:f8b0:4864:20::b34]) by gmr-mx.google.com with ESMTPS id f10-20020a25cf0a000000b00669b1eaf58dsi386332ybg.2.2022.06.26.14.33.32 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 26 Jun 2022 14:33:32 -0700 (PDT) Received-SPF: pass (google.com: domain of kaposi.ambrus@gmail.com designates 2607:f8b0:4864:20::b34 as permitted sender) client-ip=2607:f8b0:4864:20::b34; Received: by mail-yb1-xb34.google.com with SMTP id q132so13634005ybg.10 for ; Sun, 26 Jun 2022 14:33:32 -0700 (PDT) X-Received: by 2002:a25:3cc1:0:b0:66c:d89d:aedd with SMTP id j184-20020a253cc1000000b0066cd89daeddmr1254821yba.527.1656279212541; Sun, 26 Jun 2022 14:33:32 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Ambrus Kaposi Date: Sun, 26 Jun 2022 23:33:21 +0200 Message-ID: Subject: [HoTT] Call for STSMs, deadline 1 July 2022 To: moca-announce@list.it.uu.se, eutypes@cs.ru.nl, agda , coq-club@inria.fr, types-announce@lists.seas.upenn.edu, haskell@haskell.org, homotopytypetheory@googlegroups.com Cc: Danijela Simic Content-Type: multipart/alternative; boundary="0000000000001ccf9405e2608e41" X-Original-Sender: kaposi.ambrus@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=OqepQozU; spf=pass (google.com: domain of kaposi.ambrus@gmail.com designates 2607:f8b0:4864:20::b34 as permitted sender) smtp.mailfrom=kaposi.ambrus@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: , List-Unsubscribe: , --0000000000001ccf9405e2608e41 Content-Type: text/plain; charset="UTF-8" COST Action CA20111 EuroProofNet Open call for Short-Term Scientific Missions (STSMs) Dear Action members, The next STSM deadline is: 1st July 2022 Notification: 8th July. We are especially looking for applications from WG4 on the construction, management and (re)use of big libraries of formal proofs *What is an STSM?* A Short-Term Scientific Mission (STSM) is a research visit of an individual researcher from a country participating in the Action in a different country also participating in the Action. We encourage STSMs, as they are an effective way of starting and maintaining collaborations. Find all the details concerning application on https://europroofnet.github.io/grants . Write an email to us if you have any questions.Best wishes, Danijela Simic and Ambrus Kaposi EuroProofNet STSM Coordinators -- 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/CACSS4jnaphny1p-1vxUe4%3DkbAs16POBq7OTOp2t5jZWqAvnn1w%40mail.gmail.com. --0000000000001ccf9405e2608e41 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
COS= T Action CA20111 EuroProofNet
Open call for Short-Term Scientific Missions (STSMs)

Dear A= ction members,

The next STSM deadline is:

=C2=A0 =C2=A0 1st J= uly 2022

Notification: 8th July. We are especially looking for appli= cations from WG4 on the construction, management and (re)use of big librari= es of formal proofs

*What is an STSM?* A Short-Term Scientific Missi= on (STSM) is a research visit of an individual researcher from a country pa= rticipating in the Action in a different country also participating in the = Action. We encourage STSMs, as they are an effective way of starting and ma= intaining collaborations.

Find all the details concerning applicatio= n on ht= tps://europroofnet.github.io/grants . Write an email to us if you have = any questions.Best wishes,

Danijela Simic and Ambrus Kaposi

E= uroProofNet STSM Coordinators

--
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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CACSS4jnaphny1p-1vxUe4%3DkbAs16= POBq7OTOp2t5jZWqAvnn1w%40mail.gmail.com.
--0000000000001ccf9405e2608e41--