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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 24370 invoked from network); 17 Oct 2021 11:46:45 -0000 Received: from mail-wm1-x33b.google.com (2a00:1450:4864:20::33b) by inbox.vuxu.org with ESMTPUTF8; 17 Oct 2021 11:46:45 -0000 Received: by mail-wm1-x33b.google.com with SMTP id v10-20020a1cf70a000000b00318203a6bd1sf1900210wmh.6 for ; Sun, 17 Oct 2021 04:46:45 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1634471204; cv=pass; d=google.com; s=arc-20160816; b=x9s7qyg7MBv0C20kBVX7N5+ss47+X+isrL4zQ3faIpUbaYT1v5Hz5v+C+vnz/pI4Uo LKY1wG36goyjUKTy+5kwEr9Z4tFjBS4HztSUVdW2sBmg1RmdJYw58e7N4uHzPvyH030M SXuFMMRzPGp1xrc8exanKdEANCpCOVRbxTgTY7wyZtewUMZKMTfWdKnQKc055VY4ysUN hI+u95b/tbDx/BglG0evPjsrUJECOCyTcqfCvL3yAtGeNwbQj/2C6DF185h4XnjPj8/t LFUlnOeWdovqpPO6ZzHmP/poN4OnXesN5aSaMEvUqQ6TJrxp43gGutdLjgl8y0TCkSf0 /zhQ== 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:content-language :in-reply-to:mime-version:user-agent:date:message-id:references:to :from:subject:sender:dkim-signature:dkim-signature; bh=2ePXahApFfruYaABO7RYZuiMXXQnM/FqKAy8kdAyZ3g=; b=YW5fGATHfe2oARXFjYgg0lc+fo1bQuhLgP4eaSlsmZEKZZJmlJSHF4MHDLRc/kDGtt mCAbyHglCtx21gLknBy1QMkFyP4vGKrWdI2I59B0b7QiQ3c+9nsXL+tbTLYS6ad+mtA4 QBwIAn9OaNj6fXKjw2L0wiCYwWaqeEK8hUCX9zgAmC99LV4ZMBrN/UNZnOgdf0CksESm EcCcMosqCzgrHQw+w4aiZZmLi5cMMm7RnI6vzOQo/LQ/ZUdFb0oyBrpWEc+Gp2kVhxPz xkOKqkxOj+UMM4RUK8dxtwxYhOCZK49vbtt+fzKc3hE8fUvb2jZudRZDwmdaEcZBrdZz MzpQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=D6AaK46L; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::52f as permitted sender) smtp.mailfrom=benedikt.ahrens@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:subject:from:to:references:message-id:date:user-agent :mime-version:in-reply-to:content-language:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=2ePXahApFfruYaABO7RYZuiMXXQnM/FqKAy8kdAyZ3g=; b=COmHrJ1oCPKjuPhdhxQggSXywWArz3VchZqXPd4pg2HVz9Beyv3SoNyhWUY/N5S4ou 8By/ZswOgwayGYdt+vivQCuiEtFKercbklwrdUeq3/AUkEJ8sonP0zMfSw8KKguXJMj6 xOzFFLTMz2xmHsKrp5WYji/YCqQIJJuhpZ4VgqyHzppwCayN0lDsCft16GYMTaxVTC9U mpddcR1s/MbvjwYRqGu4jsn9qmuJDQ0oAt9IOTiFk3SCxrQA1LcSzoi3DsDz2pvc3xqr 3oBn9w/1ayFLLJnbqJRtgdotF6LC+rzfgNnfHRXlVcPeIVWeK/sGabhCc3eOd9MJ5Zz8 7SZg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=subject:from:to:references:message-id:date:user-agent:mime-version :in-reply-to:content-language:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=2ePXahApFfruYaABO7RYZuiMXXQnM/FqKAy8kdAyZ3g=; b=F9NMVLWRAzW00YzNVZvffsXnra7cKOTnJ53wr/C9g0GbL5I6OdwLkgIor/a86k34yH AeZ9KQ3zI5IMvnWmkQc96l/RFEUzMzF1vSS5ojAZyRPkPduUC7bGR3GbOcherce2eDXd VYcr8xU8oqeA0jEtseo4Ir6pTtgmi8iD8m/7NJrGuqYMbaK/q3SDFc/feVhVx9n8xZJr ZKFzt6jvdpYFMeZ5d9daUFOd50ik93x37Q1pmdsnS2Q3zTMPdFZrvQ6ucpgnhqqEyzC/ Li31frDiUWBXzSs5y46qLCZlf7/zPUzjvGEisqHQKL2WWa5Ep1bnlrAQe/uFn/kgeQuk +zaQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:subject:from:to:references:message-id :date:user-agent:mime-version:in-reply-to:content-language :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=2ePXahApFfruYaABO7RYZuiMXXQnM/FqKAy8kdAyZ3g=; b=IlsU/iBg2KSLXHVNKLqQTq7MTXa9ef1khninClCWnKQjUjoBVljLJxW199LIxfQTOJ K6g8YVu5qylmNEIWZLdOfXTTy7J/qXgZaS192BrVO2wulgRWwT9iRJRF9CAp4NfUcNuG zeaNHxGO8Cen5uLcEa5w8tjKxcEu5Yo/DeCS/ZnoUmICcjdrjyn49dVc4F5dmBF4bnCf MfMta/ouzZi8Gl2Ff5Q+cfdZqGEQKWCM7FoWKw+NYC0jLZFnsszsh8dxgoTDHiXvX4X1 6jrek0bQmeb6+ac5FfiJsJOUnsa4s+uSdqSCiuE5dJ1q9uvTmhxMnDoe4iqzY1XsF6NT nwhA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532JGKy8PojXLg/Xen8Rlda+yDKV7Ml46iJYoS6163VTkQKdjRUL TAOTt0hBvY8woAVnIw49bs4= X-Google-Smtp-Source: ABdhPJwH0Zj9wPdI9mUgmlbp1cep2cnlARZEUdoDL+7CaHQ94Hc99wzsEFz8Kv7ELGjva+Mqv2MqPg== X-Received: by 2002:a1c:48d:: with SMTP id 135mr24061118wme.114.1634471204682; Sun, 17 Oct 2021 04:46:44 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:5111:: with SMTP id o17ls1620347wms.3.gmail; Sun, 17 Oct 2021 04:46:43 -0700 (PDT) X-Received: by 2002:a7b:c858:: with SMTP id c24mr23405259wml.171.1634471203549; Sun, 17 Oct 2021 04:46:43 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1634471203; cv=none; d=google.com; s=arc-20160816; b=A4ySUIlmhg/2Qqfrxi1zwanfIo1onIISznH4dhTSjjhcDL8PgFihmUh7fHAh3HQscB 1vSFT6ld+e5+XElkgV+VKMt3HPyhH7RdzVFUmQzWpjzblPtx9xtET3tamosC9dsT4lm6 f5H3bbcNf6kyVKCOOCAmb/0sco2iAR4bEcrYIN1COVyrU93J+pZKeriOIfQ8R6nJjV+2 Nm/axDWF+Wyz+1dhIEZOEgRNuYS7MTLHhckR4G4GKOHemTJqffFbQ+hk9/FB00gF6GVq pAGLtJf1Zsf18in1aiizsIpycCe0zC5z5ETGgGC4YssW2eSDCvKOII1updA7mBjrsqk2 nPNA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:in-reply-to:mime-version :user-agent:date:message-id:references:to:from:subject :dkim-signature; bh=R24D/KVr8+UyWiraspab6WZckRaXr8HN2PD8166P6/k=; b=FsjtCaJ+Elj8yflbFkJ4nK2mf/Nkk5qDMUxR5AB8Rj158T3j99XfdT8FMMVNSQhOTb EWOVHZzKE2jOgOW/sPTgEmO+9LKyj8QxQ6HinPY5AXQNYUW194TVCrMX8Nkz6VNprrGB ToHI5lmOfrMVoPdBJz8iuLyD2mZqBtMPE8nLJYqvq3p53NVq7oAnV5gRO17pi5YUjgOS M3CKlxIa2Yy+lwTYl+Vn9kuLYPJarhWt9ESMWySiZ4ebc61wyCj9UETVN6j1vmLLWGO7 /ISPyJFeot4kIqr8XgD+xoQw9TzhEu2I0FZ8LzMBmlQ1C+d0NhkSijrjHYfgGWr6nCdh x7Hw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=D6AaK46L; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::52f as permitted sender) smtp.mailfrom=benedikt.ahrens@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ed1-x52f.google.com (mail-ed1-x52f.google.com. [2a00:1450:4864:20::52f]) by gmr-mx.google.com with ESMTPS id 26si1091919wmk.0.2021.10.17.04.46.43 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 17 Oct 2021 04:46:43 -0700 (PDT) Received-SPF: pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::52f as permitted sender) client-ip=2a00:1450:4864:20::52f; Received: by mail-ed1-x52f.google.com with SMTP id y30so40994552edi.0 for ; Sun, 17 Oct 2021 04:46:43 -0700 (PDT) X-Received: by 2002:aa7:ccc1:: with SMTP id y1mr35602275edt.177.1634471203219; Sun, 17 Oct 2021 04:46:43 -0700 (PDT) Received: from [192.168.0.101] (5070B429.static.ziggozakelijk.nl. [80.112.180.41]) by smtp.gmail.com with ESMTPSA id l23sm7466197ejn.15.2021.10.17.04.46.42 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 17 Oct 2021 04:46:42 -0700 (PDT) Subject: [HoTT] [Correction: participation open to anyone] A COST action for improving interoperability of computer proof systems From: Benedikt Ahrens To: homotopytypetheory@googlegroups.com References: <73181596-108f-4370-074e-f2d25ce5ca78@gmail.com> Message-ID: <719b1b3a-f54c-f399-ef4a-020e4e2deb9d@gmail.com> Date: Sun, 17 Oct 2021 13:46:41 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.14.0 MIME-Version: 1.0 In-Reply-To: <73181596-108f-4370-074e-f2d25ce5ca78@gmail.com> Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US Content-Transfer-Encoding: quoted-printable X-Original-Sender: benedikt.ahrens@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=D6AaK46L; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::52f as permitted sender) smtp.mailfrom=benedikt.ahrens@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: , Dear All, I previously sent out the call for participation below, for a network on=20 improving usability and interoperability of computer proof assistants. Back then, I said that participation is restricted - this is *incorrect*. Correct is: participation, and the possibility to receive funding, is=20 open to everyone. I apologize for my mistake, and I encourage anyone interested in the=20 topic of the network to participate in one or more of the working groups. Best, Benedikt On 30/06/2021 12:57, Benedikt Ahrens wrote: > Dear All, >=20 > You might be interested in participating in the COST action=20 > EuroProofNet, the aim of which is to improve interoperability of=20 > computer proof systems - not restricted to HoTT or type theory, but=20 > including those. >=20 > The action is led by Fr=C3=A9d=C3=A9ric Blanqui, whose message about the = action is=20 > copied below. >=20 > If you are interested, please register for participation at the link=20 > https://e-services.cost.eu/action/CA20111/working-groups/apply. >=20 > Participation is restricted to countries participating in COST - these=20 > are, in particular, EU countries, but also countries outside the EU, see= =20 > https://www.cost.eu/about/members/. >=20 > Best, > Benedikt >=20 >=20 >=20 >=20 > Dear all, >=20 > I am happy to announce the launch of a new COST action, EuroProofNet=20 > (see https://www.cost.eu/actions/CA20111/). >=20 > EuroProofNet aims at federating all the European research groups working= =20 > on proofs in order to improve the interoperability of proof systems.=20 > There are currently 6 working groups (WG): >=20 > - WG1: Proof systems interoperability. >=20 > - WG2: Automated theorem provers. >=20 > - WG3: Program verification. >=20 > - WG4: Libraries of formal proofs. >=20 > - WG5: Machine learning in proofs. >=20 > - WG6: Type theory. >=20 > You will find all the details on the objectives of EuroProofNet in=20 > https://e-services.cost.eu/files/domain_files/CA/Action_CA20111/mou/CA201= 11-e.pdf=20 > . >=20 > A COST action can fund visits to other labs, and participation to summer= =20 > schools, workshops and conferences. Anyone willing to contribute to the= =20 > goals of the action is eligible. If you are interested, you just need to= =20 > register on=20 > https://e-services.cost.eu/action/CA20111/working-groups/apply . >=20 > Best regards, >=20 > Fr=C3=A9d=C3=A9ric Blanqui, chair of EuroProofNet. --=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/719b1b3a-f54c-f399-ef4a-020e4e2deb9d%40gmail.com.