Formalization of the Algebra of Nominative Data in Mizar
Artur Korniłowicz, Andrii Kryvolap, Mykola S. Nikitchenko, Ievgen Ivanov · Annals of Computer Science and Information Systems · 2017
In the paper we describe a formalization of the notion of a nominative data with simple names and complex values in the Mizar proof assistant.Such data can be considered as a partial variable assignment which allows arbitrarily deep nesting and can be useful for formalizing semantics of programs that operate in real time environment and/or process complex data structures and for reasoning about the behavior of such programs.