Paradigmatic examples of MMT content. They are used for development and regression testing.

The language meta-level of SMGloM

documentation for SMGloM project

The slides and course notes of the course General Computer Science at Jacobs University.

Elementary set theory for the SMGloM

The SMGloM modules on linear algebra.

Graph Theory Modules in SMGloM

The glossary entries Chevahir did. May be useful at some point.

The SMGloM modules for calculus

The SMGloM modules for elementary algebra.

a research paper describing the export from Isabelle to OMDoc/MMT that is used to generate the MMT projects in this group

A MMT counterpart to the elementary math in SMGloM

General Tests (Views, Structures, etc.)

Metalogical frameworks that extend LF - the Edinburgh Logical Framework. These provide common features - e.g. record types, subtyping, or flexary functions - of logical languages at the meta-level for inheritance in LFX-specified logics.