Categorial Types for OpenMath: Overview

• Categorial types: motivations and notations

• A Categorial Type System for OpenMath

  • OMA, OMBIND, OMATTR
  • Signatures for operators, binders, and types

• Categorial Type Logic(s)

  • Inference rules, both common and uncommon
  • OpenMath: problems, and possibilities

• Conclusions

  • Quantifiers and generalizations in OM CDs

Notes: