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 2422 invoked from network); 30 Jun 2021 10:57:29 -0000 Received: from mail-wr1-x43b.google.com (2a00:1450:4864:20::43b) by inbox.vuxu.org with ESMTPUTF8; 30 Jun 2021 10:57:29 -0000 Received: by mail-wr1-x43b.google.com with SMTP id a4-20020a0560001884b0290124b6e4a437sf716419wri.16 for ; Wed, 30 Jun 2021 03:57:29 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1625050648; cv=pass; d=google.com; s=arc-20160816; b=O/jMrgHTqJOy8yXG8dVtD+p3ErFhhQbAeMsXHQMjJBVYesfowBVa8IqrOf0qpg4h7R BSGO2ro6SA71nTQG7L1b44Lyxr+fo/tZ9ejvGDbKVrv3mNBVxPAQAZU3Eb0/5QF7B/A2 LUEmukY2pW9iCgyIBQBDnEqaUv59b8JD67coKOj2hl9nuTEbiRcPBOMZspmWXIDR0rSE 0svr6OW64W1S+pFWE/g+aQE4p0Ldt6PtV2gLVLqS+NfHXPmo8zw7nK3wOanzYEEIapJX S7s38qoFRXcWtFkuxHrQe6yHca6YFTn17xSUDsUAe+nleNywEeeqDmX3uFGcb15kWKjx tPMA== 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 :mime-version:user-agent:date:message-id:subject:to:from:sender :dkim-signature:dkim-signature; bh=TyemSY9LaBloSgQPm3GQ0SljwIIqmQWN9CcjesP7j+o=; b=DO2NKsG31VnM2PnGJMdQFe3XJswwGWj3rEg9UNm96jbUzQlgSe0/W/xCWX/dDj+Irr SVvVGVT0QdLq3OoZhB3w+sIjwuuHx3bQMI3c5RUxXUnmElguc2jwPb10u6u0hEA3iyoa gS9WFaTaOXVTodxf7AqjYWeLFX8ME7bjXVzlwklpQBWLoJHRsSJSLo4BIwQIQBzxhMLP PClB1atyyO1sSjrwzYzB+BKZyBWh0Ar+szdhT+0pADhfo4atGzmunz5HJ3Qy2MCXqiXV CFNBaC8tizb/X9I6zAstxyYgiiObGNU1RhHiekFG0eAniplQBqyRdNFXrS3I1An/Yn2D ywAw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=Klo4Jx7L; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::532 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=20161025; h=sender:from:to:subject:message-id:date:user-agent:mime-version :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=TyemSY9LaBloSgQPm3GQ0SljwIIqmQWN9CcjesP7j+o=; b=rcsdabXO2Lm/mQcdiOhrJAXEwEedbFskb06FY+E3k3bcgNbJYiHMyTjrd0jipLI8TE f5xhR8JNF8S7ou2iWnXVuKCXabmX5M6dowQRy8b87zyWscdmjD3MsQJpRXVO0gAej/aA fZLHCI8VjOVvKmQRK5Tsa8J3Rrf98MVX7S/a2IvY3z99AuS/i6cOlCkGvCnxl9AZeFjX xWJnMpKlrZBtLn8n2MQ/Lvn7Suk1RkG52m4YaBfLdi2wpg4/6pASFSqiDNhyibU5pOPn nDpCHPAxe0Yo5EfhprWRYTe5ofApYQxeuab0jcHyncR5dLji1ePq94ggKGBxkbV0VCIY +gsQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:subject:message-id:date:user-agent:mime-version :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=TyemSY9LaBloSgQPm3GQ0SljwIIqmQWN9CcjesP7j+o=; b=iRIVwYbRH2DPHgWiuDF6HU0YkV+ZwnKt6FkThfPbWtQWG383AeUM8HuCOsVO/7qamt EtB6ueihw9oaUSh0Xco8Mrw3IZ0AOJX1MurTPz0s7fnyuxvqVISXzgiBq/quTq+ky4kw G5J2jU0p0py61ByIwFOPH75RaiO96/D2QV1JknZbrNeNfJtElEoBVoKXw/oksCCsY1dR HVmB+nbmzx14AuXNAMZS3e5mnbGVn7dsB8xTR2QW/zNVS342QTixgHOWXlr3ylYRWbAI z+6WB5BNd82fSeUmxYPfFb6ZGKkik76n0VMs7X7AZ7JKROl+vzNjHAoUDSdqFJtYs3ak 6pJw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:subject:message-id:date :user-agent:mime-version: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=TyemSY9LaBloSgQPm3GQ0SljwIIqmQWN9CcjesP7j+o=; b=sfeifybhBbGxj79nr5tm6unupJjVemoE8yk1Du8t3WwLhV9U/85kw0+vfA0e8sT7ns hNJo/m45KcB7XeV8N8habD7zUWb3Hc8bvO0qN+9gf3RJCPrfGe6WlnVrTcJO/2Rmm92R cw1cgfDtr0W78DosO9ErydQ4Pfq1ctFtvwepJlK6E3jbMPEKGDwbptUXWHaS7Mkl2PDV anA92RSVDynWFU6Y34L7qCmROBqqH+QzTn/qOFu67/pw9TOA9cepQpKZjOIZtedbeDCl zmJeId1gGOONJqG7RlJqls00TYRBl/RAqKlFBc8bdhrgLLhK5GOqnGgZKkEJ73KH2WVt GOGg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532Bb4ROKvgNQ4CBao12F7EGoh0SJOWkOpAye/3WVreFtOX0JDhP 4oBhP3kg24jQ0eYbHAnvjp4= X-Google-Smtp-Source: ABdhPJzw6Djt+O1pDrHK3cUDDEf560/n340iP6yTaLEOlkgPGlneqgRM4kMCEeseC8wM+410a4YSyQ== X-Received: by 2002:adf:ee10:: with SMTP id y16mr1179067wrn.99.1625050648105; Wed, 30 Jun 2021 03:57:28 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:1c90:: with SMTP id k16ls63718wms.2.canary-gmail; Wed, 30 Jun 2021 03:57:27 -0700 (PDT) X-Received: by 2002:a7b:c194:: with SMTP id y20mr10028195wmi.125.1625050647245; Wed, 30 Jun 2021 03:57:27 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1625050647; cv=none; d=google.com; s=arc-20160816; b=Ry26UzCllR7HWmgaDYkewhp1OLmhhk0KxnBnWU2FVbmy3dTY+k1uT4o71P/hqWxw6i YWOnq6r67eZuQATkKgAvhj2xkA/hIFhen3Ut0cb5zl/iz1RboDBoZDSwtN36n9DKnI9p MKaquodfRK1NM0ecT8LdNRlADmKoqjCDagaCuov66O35rbPoG6UTdudFORsYw+aeJVbx QmLQaSpiVr8L8B8Qh37dn9qRKw40s3TcKeh699miHvF4RJ9wB5SXVC119Hjt0rGkBGL6 5DrQELiBvAgBX242jL0oZC6Osl/B1EOZTigS6tW6xV+uSozSjyNKDy5bAHLlOjy0QmR3 c5EA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:mime-version:user-agent :date:message-id:subject:to:from:dkim-signature; bh=bo49ryjl4zUhNTfYQ1W+oAuZyI8aQNpnaIdWOy911TI=; b=yz4X7SklRXdDWm76PhmRPttxp9vM4Fe4V/0AO8VNY0J12Qiq9405FTcsGmb4ihfpI7 ffTtncPB2kQ1lSXw12CrQLm0+Mte+CKp5JrYBBctADWo6D31EhP6uCLcZx+jZmtHduSt wvJdWg8edOaZiMn72qveUwFH6LyzJEc/4fvTM0bIi6g81V4QOH0J7/j9x+coWE6ahoWw 7VW9SCGuMNnOTUatWcYIUNSk/aFtkmjoRXhjduxdlry/FmOAqyb6eNMjOPz4ON+GjUpT KarSJ9+hUyxISi8WGCSyrpop9rikWw7SRcoF/LUr0HaVs37VN6M9N93sXk31fQ5vYRoJ HOrg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=Klo4Jx7L; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::532 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-x532.google.com (mail-ed1-x532.google.com. [2a00:1450:4864:20::532]) by gmr-mx.google.com with ESMTPS id c4si326159wml.4.2021.06.30.03.57.27 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 30 Jun 2021 03:57:27 -0700 (PDT) Received-SPF: pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::532 as permitted sender) client-ip=2a00:1450:4864:20::532; Received: by mail-ed1-x532.google.com with SMTP id w17so2575133edd.10 for ; Wed, 30 Jun 2021 03:57:27 -0700 (PDT) X-Received: by 2002:a05:6402:451:: with SMTP id p17mr42489114edw.332.1625050646935; Wed, 30 Jun 2021 03:57:26 -0700 (PDT) Received: from ?IPv6:2001:a62:4c5:4801:3d2e:45b3:5ad8:8275? ([2001:a62:4c5:4801:3d2e:45b3:5ad8:8275]) by smtp.gmail.com with ESMTPSA id v24sm685410eds.39.2021.06.30.03.57.25 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 30 Jun 2021 03:57:26 -0700 (PDT) From: Benedikt Ahrens To: homotopytypetheory@googlegroups.com Subject: [HoTT] A COST action for improving interoperability of computer proof systems - members wanted Message-ID: <73181596-108f-4370-074e-f2d25ce5ca78@gmail.com> Date: Wed, 30 Jun 2021 12:57:25 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.11.0 MIME-Version: 1.0 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=20161025 header.b=Klo4Jx7L; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::532 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, 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. The action is led by Fr=C3=A9d=C3=A9ric Blanqui, whose message about the ac= tion is=20 copied below. If you are interested, please register for participation at the link=20 https://e-services.cost.eu/action/CA20111/working-groups/apply. 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/. Best, Benedikt Dear all, I am happy to announce the launch of a new COST action, EuroProofNet=20 (see https://www.cost.eu/actions/CA20111/). 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): - WG1: Proof systems interoperability. - WG2: Automated theorem provers. - WG3: Program verification. - WG4: Libraries of formal proofs. - WG5: Machine learning in proofs. - WG6: Type theory. 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/CA20111= -e.pdf=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 https://e-services.cost.eu/action/CA20111/working-groups/apply = . Best regards, 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/73181596-108f-4370-074e-f2d25ce5ca78%40gmail.com.