MMT - Meta-Meta-Theory and/or Tool:
A Framework for Defining and Implementing Logics

Florian Rabe

LRI, University Paris-Sud, France
Computer Science, University Erlangen-Nuremberg, Germany

MMT is a framework for designing formal languages and building knowledge management applications for them. It systematically avoids a commitment to a representational paradigm, a particular concrete or abstract syntax, or a particular semantics and thus naturally subsumes type theories, logics, set theories, ontology languages, etc. Despite this high degree of generality, MMT includes generic solutions to deep problems including IDE, web browser, module system, and type checking. Therefore, designing logics and applications inside MMT can yield very strong systems at extremely low cost.


Florian Rabe, Winner of the 2015 Unilog Contest The Future of Logic

I. Overview and demo
Optionally bring your notebooks to install MMT
II. Language Design in MMT
III. Application Development in MM

  • Florian Rabe, "The Future of Logic: Foundation-Independence" Logica Universalis, March 2016, Volume 10, Issue 1, pp 1–20.
  • Florian Rabe, "How to Identify, Translate, and Combine Logics?" Journal of Logic and Computation, 2014.