A Type System for OpenMath
Olga Caprotti, A. M. Cohen · 1999
This document describes one possible type system for OpenMath that is an adaptation of the Extended Calculus of Constructions. Including formally specified type information in OpenMath Content Dictionaries allows to assign precise semantical meaning to OpenMath objects corresponding to mathematical notions and therefore to perform automatic validation on OpenMath objects. A Type System for OpenMath (Task: 1.3) iii ESPRIT project 24969: OpenMath iv A Type System for OpenMath (Task: 1.3) ESPRIT project 24969: OpenMath