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
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.
Florian Rabe is a senior researcher in computer science at
University Erlangen-Nuremberg (Germany) and University Paris-Sud
(France). He received his PhD in 2008 and his habilitation in 2014
from Jacobs University Bremen (Germany).
His research centers around formal systems of all kinds such as specification languages, logics, or programming languages. He focuses on the uniform treatment of their proof theories, model theories, and implementations as well as on knowledge management, module systems, and translations for them. His methods extend and combine diverse research strands including logical frameworks, algebraic specification, and computer mathematics. His main contributions are integrated in the MMT language and system for designing and applying formal systems.
Host: Fairouz Kamareddine