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 autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 15061 invoked from network); 15 May 2020 19:03:05 -0000 Received: from mail-wr1-x437.google.com (2a00:1450:4864:20::437) by inbox.vuxu.org with ESMTPUTF8; 15 May 2020 19:03:05 -0000 Received: by mail-wr1-x437.google.com with SMTP id h12sf1598865wrr.19 for ; Fri, 15 May 2020 12:03:05 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1589569382; cv=pass; d=google.com; s=arc-20160816; b=LFvILKO6+WS4tIKFCIjo0+G19dYmiJeodrq6sf0asNQbN57HThuic1PmGzchLbtuNj Gl5wrKpZApYG+2Deg6NjQ/6M+3W0JcxKZZhG/xXO/af1NuhPiwDHDwHjJAruK/bpBwIq cyGeOFin6UWiY8hPPqJiPS9x3NzV1aNp0HcrJ5x95cCwYuP9ugKn/M/dLqS5glxKcPaV 9FUotbsxWYcWADbMwj/Gf8bNy2MgPXtECzW/QFgkmwCKXYlu2bF4hX8Khyuk04FW8uoP WdB/5U6jYg7yOo4JA08DtJRZZRfog2ERdT7u6PIfbWKNM8g7badHTdWvDnrDMFcAEUF+ 1lbg== 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:to:subject :message-id:date:from:mime-version:sender:dkim-signature; bh=nVNZM69MPy2H82jcNKKg+2FS1gsjLc1phDB9j7H3pcY=; b=p4RuvaOR8iJpZEZvOuMzig2uhNIZGVgdyTp6ufEsiFU1P1R4S83fS+HpK3cVwqq9cA nW1XN+6u1kT14R3II46oIh1TMJhHnmOtFEKw0QZEQVQauNv4rPpDC9RC+qk0jnQ3XU4A 2cmBqy0XY84iLTHrrXycCv91Yk/hy+4ghykfTF2jYcmW8wvVqt3DYrNfunRDfrqWIlUT ULIbeCzukuvATm6WIGmbVpGAlhiKy5okOgWs7x/kX8a1ZBRx1B1kooKAySELasmV6gq0 k2UPzy+tTsdN1PFmG/tw/aCDnrljZCg1v0Yx/SsLh8gs1A6KF4liTUZrZbSaprCNbcGE 4b/g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=vzysNrTT; spf=neutral (google.com: 2a00:1450:4864:20::135 is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) smtp.mailfrom=andrej.bauer@andrej.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:from:date:message-id:subject:to :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=nVNZM69MPy2H82jcNKKg+2FS1gsjLc1phDB9j7H3pcY=; b=TdTKwVkZTBnbBEo//WTgZWohVcN0To+WvErjkHNZhRkhTNFY/fGR4eBk9azxI3GrM3 yO4l4ClzUWeQvPbAPLp4Bap2vKSIqk4jVKvu30NiDUyVa4Go95QP/UcnYY1SIGUqwkef QYDFyRbMT57xa9eS6Ct22aHgM43a6qPJ4zgtMWnSUW8hejKeMuiD/FFsKn+7TUa2pa85 NbmhHSfyNv2C3TAm371Rx6ivLXPAes3kUXIt12zV2Q5YYFysyvHX5ytXm5U78iPfS3Fm SOhKOVGKzTbp2Z9E7z7H8Hm4wRurkcpnGYrH0WFODRMXEKNZ8nTgU/9viDiAaI+f77b4 KMSg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to: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=nVNZM69MPy2H82jcNKKg+2FS1gsjLc1phDB9j7H3pcY=; b=JrQBpC9C856OjOzs+rBzDS8eE/LI20zuON5eTupi4MmbepbyWcEJi726VWID+ouJ5U lW/8OTAjuahU9a1TyMerL/WE8GzIH3ccv66W/E3c2dbAfFN3kCSj2zQuWBPNiUt0vW5M UJuNRso3z4ts3E9fSsI3khZv0i5r/t1yYsgZlt76HsHYOmJPaREsgxYkpNsyWOD6Uh5q ssXV1gEqukMltFbazNc3YcBmmafiqmeVCaTddsOcQ/rMLc+JTcAnjjHlV00P7K9UTU6Z 7a5tIs0td3nYtXraVOEAk6ReftN8gRcbxbMdyBeKW9WewNrPbGkrT0BORvfdXUpJJ+gD S6Pg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM531ng2IVhzWa6VUCDqwPlCINPeodHAQp3c5JF7kReCY+JUtj0K5f rR/0UBcOEGSUAzllX3vGYHw= X-Google-Smtp-Source: ABdhPJzGMUTaButmx1n0oI9RfDGvjgO8sMYwowWSMn24HJAfjjSahGbH8cGH1AxLKlpLozAK4BkBvw== X-Received: by 2002:adf:e582:: with SMTP id l2mr6151862wrm.392.1589569382378; Fri, 15 May 2020 12:03:02 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:6186:: with SMTP id v128ls1691330wmb.2.gmail; Fri, 15 May 2020 12:03:01 -0700 (PDT) X-Received: by 2002:a1c:32c5:: with SMTP id y188mr5956200wmy.16.1589569381814; Fri, 15 May 2020 12:03:01 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589569381; cv=none; d=google.com; s=arc-20160816; b=KgpnsvADj9GlcuVsWaPjj/0Uh7/sEIOkgUB2A722X94KJhTQtXaSF/VCyi7GeY+a6H PBbuKoaa65DYF71klW77riyMD1zqoOZ8Z6YdajnRfF94HJ6ljuUA9LKTYjQzfrQ9Q5rm r93P4od2Mv7Lq4IF4VxUyfsnmUkqQnga0HDmMFF6bMX5RNc+x3Dor8qy3mASjnd4eJqb 114geGrphGYWSgQ1a2DTRk8PanB6ocSKRyeugEYa4VF4teJDgJxLtjJe7QSQYX2gWFwA 0OLxSUsphYo4F7OnwpRGt6FQr6BD9Ci5V0/XT9BQsBkkFilHzuV/bwpdvBrw+zIkXpwi Oahw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :mime-version:dkim-signature; bh=rrc0CKpW2tF66M8y3gNnrXmSTK8qwd0l1yJPC/F4ECo=; b=ari1GF9y8tN00rY0nVedqKTsNOja7bohoNuPDdhL2kEzmSNtX/Iyx9lkWaJfJ2sG7S K493iGjbP6iGmUWfofhs13AdEcoezxCa0UjBS74D7t0tjrL+Nve2PD24G244QpcUwtQR c5uSvEuyRzmndkD17jHTygG9xK935ODHTAxVI0zJ30JTXvFU5wTfHdnX4Wt3LweRIX9r hW9XMi/uVO02799jqFpDrj0h1GTJ9jZLtcIHlz8bTESCuU8EmASmkoc8ttdI4i2qBgB0 W0KAe/KhCf1/AhCR5QzZvfwXNeA4NLbxkgR1bClnHQJIXjmdmM2FFUWWX7tmAn35iRmC DSFA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=vzysNrTT; spf=neutral (google.com: 2a00:1450:4864:20::135 is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) smtp.mailfrom=andrej.bauer@andrej.com Received: from mail-lf1-x135.google.com (mail-lf1-x135.google.com. [2a00:1450:4864:20::135]) by gmr-mx.google.com with ESMTPS id q70si756134wme.0.2020.05.15.12.03.01 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 15 May 2020 12:03:01 -0700 (PDT) Received-SPF: neutral (google.com: 2a00:1450:4864:20::135 is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) client-ip=2a00:1450:4864:20::135; Received: by mail-lf1-x135.google.com with SMTP id 202so2708693lfe.5 for ; Fri, 15 May 2020 12:03:01 -0700 (PDT) X-Received: by 2002:ac2:5490:: with SMTP id t16mr3350335lfk.178.1589569380974; Fri, 15 May 2020 12:03:00 -0700 (PDT) MIME-Version: 1.0 From: Andrej Bauer Date: Fri, 15 May 2020 21:02:45 +0200 Message-ID: Subject: [HoTT] Every proof assistant talk announcement: MMT (Florian Rabe) To: "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: andrej.bauer@andrej.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=vzysNrTT; spf=neutral (google.com: 2a00:1450:4864:20::135 is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) smtp.mailfrom=andrej.bauer@andrej.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: , It is my pleasure to announce the second in the series of online seminars on proof assistants. MMT: A Foundation-Independent Logical System Time: Thursday, May 21, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2) Location: online at Zoom ID 989 0478 8985 (https://zoom.us/j/98904788985) Speaker: Florian Rabe (University of Erlangen) (https://kwarc.info/people/frabe/) Proof assistant: The MMT Language and System (https://uniformal.github.io/) Abstract: Logical frameworks are meta-logics for defining other logics. MMT follows this approach but abstracts even further: it avoids committing to any foundational features like function types or propositions. All MMT algorithms are parametric in a set of rules, which are self-contained objects plugged in by the language designer. That results in a framework general enough to develop many formal systems including other logical frameworks in it, enabling the rapid prototyping of new language features. Despite this high level of generality, it is possible to develop sophisticated results in MMT. The current release includes, e.g., parsing, type reconstruction, module system, IDE-style editor, and interactive library browser. MMT is systematically designed to be extensible, providing multiple APIs and plugin interfaces, and thus provides a versatile infrastructure for system development and integration. This talk gives an overview of the current state of MMT and its future challenges. Examples are drawn from the LATIN project, a long-running project of building a modular, highly inter-related suite of formalizations of logics and related formal systems. After the talk, the video recording will be made available. Also see the anouncement on my blog at http://math.andrej.com/2020/05/15/mmt-a-foundation-independent-logical-syst= em/ The spring schedule of talks is planned as follows: May 28, 2020: Brigitte Pientka - Beluga June 11, 2020: Conor McBride - Epigram 2 June 25, 2020: William J. Bowman, Cur July 2, 2020: Anders M=C3=B6rtberg - cubicaltt (to be confirmed) July 9, 2020: Jon Sterling - redtt (to be confirmed) With kind regards, Andrej --=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/CAB0nkh2Q_YFsZEZDq0qx9EudT3dO5yaSFPWP5hVWtJSgykkrnQ%40ma= il.gmail.com.