Defining Formal Systems in MMT

Florian Rabe
University Erlangen-Nuremberg, Germany, and University Paris-Sud, France.

Friday 31 May 2019
14:15 - 15:15
Room 3.06, Earl Mountbatten Building

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.

Bio

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.

Website.

Host: Fairouz Kamareddine