Project Description: 

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.

Project Start Date: 
January, 2007