Categorial Type System: Summary

• Categorial type system is possible and useful for OpenMath

  • factors out structural semantics common to all
    • Type logic on “atoms” orthogonal, pluggable (I hope)
  • supports “radical lexicalism”
  • both coarse and fine grained types/signatures
    • similar to parallel content/presentation options
  • modifies both STS and ECC, slightly
    • Simpler than ECC, more complete than STS
  • Flushes out a couple of hard-to-find bugs

Notes: