menu
MMT
A framework for representing declarative languages such as logics, type theories, set theories, etc.. The MMT API implements complex algorithms generically for any language in the framework.

Start: March 2011


Prof. Dr. Florian Rabe
Dr. Dennis Müller
M.Sc. Tom Wiesing
Dr. Mihnea Iancu
Dr. Fulya Horozal
Prof. Dr. Michael Kohlhase
M.Sc. Navid Roux

Funded by:
OAF
ODK
LATIN
MathSearch

MMT is a framework for representing declarative languages such as logics, type theories, set theories, etc.. It achieves a high level of generality by systematically avoiding a commitment to a particular syntax or semantics. Instead, individual language features (e.g., λ-abstraction, conjunction, etc.) and syntax features (keywords, notations, etc.) are defined as separate, reusable modules, from which individual languages are assembled. These modules can be declarative by specifying features as Mmt theories or programmatic by providing individual rules as plugins.Despite this high degree of abstraction, it is possible to implement advanced algorithms generically at the MMT level. These include knowledge management algorithms (e.g, IDE, search, change management) as well as logical algorithms (e.g., parsing, type reconstruction, module system). Thus, we can use MMT to obtain strong implementations of declarative languages at extremely low cost.Moreover, the focus on modularity and language-independence enables system integration, where MMT can mediate the exchange of knowledge across different foundational systems and concrete syntaxes.See here for the MMT homepage.