[HoTT] Every proof assistant talk announcement: MMT (Florian Rabe)

[HoTT] Every proof assistant talk announcement: MMT (Florian Rabe)

[Andrej Bauer]

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.