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.

I. Overview and demo
Optionally bring your notebooks to install MMT