Implementation of the Composition-nominative Approach to Program Formalization in Mizar - Ievgen Ivanov; Artur Kornilowicz; Mykola Nikitchenko (Computer Science Journal of Moldova, 2018)
In this paper we describe an ongoing work on implementation of the composition-nominative approach to program formalization in Mizar proof assistant based on the first-order logic and axiomatic set theory. The further aim of this work is development of a formal verification tool for software which processes and communicates with complex forms of data.