Global, Regional, and Local Contexts.

We introduce UniFormal, a formal language for mathematical knowledge representation that continues the evolution of OpenMath and MMT. It is motivated by the lack of identifiers in these languages that exhibit the scoping behavior needed for, e.g., the fields in a record or the variables in a polynomial. Its core feature is a separation of identifiers and associated contexts into three levels: The global context maintains the usual toplevel declarations that can be imported across libraries and nested packages via qualified names. The local context maintains the usual α -renamable bound variables with narrow syntactic scope. The novel regional context sits in between these and maintains the identifiers of the current theory. A stack of regional contexts is used to allow for expressions that move between regions, e.g., when applying a theory morphism to transport an expression from one theory to another. We present a minimal language in this style, focusing on the general intuitions underlying the design. We anticipate it to be extended flexibly towards specialized aspects of mathematical knowledge such as programming languages or theorem provers to enable interoperability through their shared core concepts. This approach has already proved successful in the design and implementation of a UniFormal programming language.