Florian Rabe: Defining Formal Systems in MMT

Datum objave: 10. 6. 2019
Seminar za temelje matematike in teoretično računalništvo
Četrtek, 13. 6. 2019, od 14h do 16h, učilnica 3.07, Jadranska 21

Pozor: dobimo se ob nestandardnem času, v četrtek 13. 6. 2019 ob 14h v 3.07! 

Attention: we meet at a non-standard time on Thursday, 13. 6. 2019 at 14h in 3.07! 

Abstract: Logical frameworks like Twelf and Isabelle are meta-formalisms in which the syntax and semantics of object logics and related formal systems can be defined.
This allows developing support services like theorem proving generically and reuse them for many object logics.

MMT follows this tradition but abstracts even further than previous frameworks: it avoids foundational commitments as much as possible and does not build in any primitive features like function types or propositions.
Instead, all MMT algorithms are parametric in a set of rules, which are supplied by the language designer as self-contained objects in the underlying programming language.
That makes it easy to define language features that existing frameworks cannot express.

In this talk, I describe the design of MMT and give a few concrete object logic definitions in detail.