Angles of MMT, each one sentence

• MMT is a scalable module system for formalizing knowledge.
• MMT/LF induces a module system over LF.
• MMT is a foundation-independent framework for representing declarative languages such as logics, type theories, set theories.
• The MMT API implements complex algorithms generically for any language in the framework.
• MMT allows rapid prototyping of formal systems
• MMT allows formalizing knowledge declaratively and modularly with an open-world assumption in mind.
• MMT theories represent knowledge... (in parentheses: inductive datatypes as found e.g. in Coq represent knowledge...)
  • declaratively (inductively)
  • modularly (monolithicially)
  • with an open-world assumption (closed-world assumption)
• MMT views represent knowledge
  • declaratively
  • modularly
  • with a somewhat closed-world assumption (due to compositionality)
• MMT views v: S -> T may represent
  • compositional language translations from S-terms to T-terms
  • special cases of meta theorems (e.g. soundness)
  • S being more general than T (compositionally, so, see Navid's bsc thesis)
  • T implementing S via v