The FMathL type system
Peter Schodl, Arnold Neumaier · 2011
The FMathL type system is a common generalization of context-free grammars and algebraic data types in programming languages, and consists of a system of declared categories and types. The type declarations themselves are represented via typed objects, making the whole typing self-consistent. Correctness of types can be checked in linear time. The type system is defined within a framework for representing semantic content, specially designed to naturally represent arbitrary mathematics. Information is represented via semantic units (sems) relating objects, an undefined notion that may be interpreted as elements of the domain of a semantic mapping. Meaning is conveyed by means of type declarations that specify how objects may relate with each other.