MMT Tutorial (organizers Florian Rabe, Mihnea Iancu, Dennis Müller)

MMT is a framework for designing formal languages and building knowlwedge 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 checker.

Therefore, designing knowledge representation languages and applications inside MMT can yield very strong systems at extremely low cost.

The tutorial will take place Friday morning and thus consist of 2 sessions separated by a coffee break.
The 2 sessions work together but can be attended independently.
The sessions will be hands-on, and participants are encouraged to bring their notebooks.

Session 1 (9:00-11:00): Language Design in MMT

• install MMT and the MMT IDE,
• use MMT to define the syntax and semantics of a formal language (e.g., first-order logic) in a way that maximizes the reuse of features, applications, and content,
• build a small library in that formal language.

Session 2 (11:00-12:30): Application Design with MMT

• Developers can make major changes even to kernel behavior: This mini-demo turns MMT into a rewrite system.
• All functionality is available via open high-level interface: This mini-demo shows a web-based editor that uses the JAPI for MMT's query language.
• Import/export workflows support system interoperability: This mini-demo shows how to use MMT as an OpenMath Content Dictionary editor by adding an exporter to OpenMath.