From: Andrej Bauer <andrej.bauer@andrej.com>
To: "HomotopyTypeTheory@googlegroups.com"
<homotopytypetheory@googlegroups.com>
Subject: [HoTT] Every proof assistant talk announcement: MMT (Florian Rabe)
Date: Fri, 15 May 2020 21:02:45 +0200 [thread overview]
Message-ID: <CAB0nkh2Q_YFsZEZDq0qx9EudT3dO5yaSFPWP5hVWtJSgykkrnQ@mail.gmail.com> (raw)
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-system/
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örtberg - cubicaltt (to be confirmed)
July 9, 2020: Jon Sterling - redtt (to be confirmed)
With kind regards,
Andrej
--
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/CAB0nkh2Q_YFsZEZDq0qx9EudT3dO5yaSFPWP5hVWtJSgykkrnQ%40mail.gmail.com.
reply other threads:[~2020-05-15 19:03 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=CAB0nkh2Q_YFsZEZDq0qx9EudT3dO5yaSFPWP5hVWtJSgykkrnQ@mail.gmail.com \
--to=andrej.bauer@andrej.com \
--cc=homotopytypetheory@googlegroups.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).