Compiling OpenMath Type systems to RelaxNG Grammars

OpenMath has long had an infrastructure for specifying types of symbols in the content dictionaries. But these types have not been used for validation of formulae in practice. Surprisingly, even though the official OM CDs have been typed with James Davenport's Simple Type System, not all formulae in the examples are well-typed, since general-purpose type checkers are missing and those that exist are not integrated into authoring tools and workflows.

To alleviate this situation, we will present a simple way to compile (various aspects of (an extension of)) STS types into RelaxNG grammars, so that type checking can be reduced to schema validation, which is better integrated with the XML workflow.

Author(s): 
Michael Kohlhase
Publication_details: 
3rd JEM Workshop, 31 Jan.-1 Feb. 2008, Barcelona Spain
Type: 
Slide presentation
Date: 
2008/01/15
Partner_node: 
Jacobs University
VedleggStørrelse
sts-relaxng.pdf190.76 KB