We propose extensions and corrections of the syntax and semantics of OMDoc that are necessary to define a formal semantics of OMDoc theory graphs. Since OMDoc theories are also OpenMath content dictionaries, this provides a module system and rudimentary syntax checking for OpenMath.

Our proposal includes a new constructor for OpenMath objects that is needed in the context of this module system. Together with related, so far unpublished work, this contribution provides a formal semantics and full type checking for OMDoc theory graphs.