Florian Rabe: Defining Formal Systems in MMT
Source: Mathematics and theoretical computing seminar
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.