Type Systems for OpenMath

Several formal type systems exist for OM
- a) Support for many different type logics (pro)
- b) Different meanings for "apply" and "bind” (con)
Is (b) really necessary for (a)?

A Categorial Type Logic for OpenMath

Compositional structural semantics for OM: OMA,OMBIND,OMATTR (incl. type attribs)
Simple common core for all OM type systems
”Plug-in” detailed type systems for symbols only