Every proof assistant: MMT
source link: http://math.andrej.com/2020/05/15/mmt-a-foundation-independent-logical-system/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Every proof assistant: MMT
I am happy to announce the next seminar in the "Every proof assistant" series.
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
Speaker: Florian Rabe (University of Erlangen)
Proof assistant: The MMT Language and SystemAbstract: 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 rapidly 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.
The spring schedule of talks is planned as follows:
Comments
Would it be possible to get the full slide deck?
Post a comment:
$⋯$
for inline and $$⋯$$
for display LaTeX formulas,
and <pre>⋯</pre>
for display code. Your E-mail address is only used to compute
your Gravatar and is not stored anywhere.
Comments are moderated through pull requests.
Name
Website
Comment
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK