{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T00:12:00Z","timestamp":1770682320782,"version":"3.49.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319672281","type":"print"},{"value":"9783319672298","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,9,7]],"date-time":"2017-09-07T00:00:00Z","timestamp":1504742400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-67229-8_16","type":"book-chapter","created":{"date-parts":[[2017,9,5]],"date-time":"2017-09-05T21:53:54Z","timestamp":1504648434000},"page":"176-186","source":"Crossref","is-referenced-by-count":12,"title":["Formalization of the Nominative Algorithmic Algebra in Mizar"],"prefix":"10.1007","author":[{"given":"Artur","family":"Korni\u0142owicz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrii","family":"Kryvolap","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mykola","family":"Nikitchenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ievgen","family":"Ivanov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,7]]},"reference":[{"key":"16_CR1","unstructured":"International Telecommunication Union: Overview of the Internet of Things. ITU-T Recommendation Y.4000\/Y.2060, June 2012. http:\/\/handle.itu.int\/11.1002\/1000\/11559"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Wiedijk, F. (ed.): The Seventeen Provers of the World. Lecture Notes in Artificial Intelligence, vol. 3600. Springer, Heidelberg (2006)","DOI":"10.1007\/11542384"},{"key":"16_CR3","unstructured":"The CompCert project. http:\/\/compcert.inria.fr"},{"key":"16_CR4","unstructured":"CakeML: A verified implementation of ML. https:\/\/cakeml.org"},{"key":"16_CR5","unstructured":"The seL4 Microkernel. https:\/\/sel4.systems"},{"key":"16_CR6","unstructured":"CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: OSDI 2016 Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation, Savannah, GA, USA, 2\u20134 November 2016 (2016)"},{"key":"16_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Kryvolap, A., Nikitchenko, M., Schreiner, W.: Extending Floyd-Hoare logic for partial pre- and postconditions. Communications in Computer and Information Science, vol. 412, pp. 355\u2013378. Springer (2013). http:\/\/dx.doi.org\/10.1007\/978-3-319-03998-5_18","DOI":"10.1007\/978-3-319-03998-5_18"},{"key":"16_CR9","unstructured":"Korni\u0142owicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: An approach to formalization of an extension of Floyd-Hoare logic. In: Proceedings of the 13th International Conference on ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer (ICTERI 2017), Kyiv, Ukraine, 15\u201318 May 2017. CEUR-WS.org (2017). http:\/\/ceur-ws.org\/Vol-1844\/10000504.pdf"},{"key":"16_CR10","unstructured":"Nikitchenko, N.S.: A composition nominative approach to program semantics, IT-TR 1998-020. Technical report, Technical University of Denmark (1998)"},{"key":"16_CR11","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/BF01071436","volume":"5","author":"V Glushkov","year":"1965","unstructured":"Glushkov, V.: Automata theory and formal transformations of microprograms. Cybernetics 5, 3\u201310 (1965). (in Russian)","journal-title":"Cybernetics"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Floyd, R.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, vol. 19, pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"issue":"10","key":"16_CR13","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C Hoare","year":"1969","unstructured":"Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). doi: 10.1145\/363235.363259","journal-title":"Commun. ACM"},{"issue":"2","key":"16_CR14","first-page":"263","volume":"23","author":"M Nikitchenko","year":"2017","unstructured":"Nikitchenko, M., Shkilniak, S.: Algebras and logics of partial quasiary predicates. Algebra Discret. Math. 23(2), 263\u2013278 (2017)","journal-title":"Algebra Discret. Math."},{"key":"16_CR15","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-319-13206-8_6","volume":"469","author":"V Skobelev","year":"2014","unstructured":"Skobelev, V., Nikitchenko, M., Ivanov, I.: On algebraic properties of nominative data and functions. Commun. Comput. Inf. Sci. 469, 117\u2013138 (2014). doi: 10.1007\/978-3-319-13206-8_6","journal-title":"Commun. Comput. Inf. Sci."},{"issue":"3","key":"16_CR16","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10817-015-9345-1","volume":"55","author":"A Grabowski","year":"2015","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Four decades of Mizar. J. Autom. Reason. 55(3), 191\u2013198 (2015). doi: 10.1007\/s10817-015-9345-1","journal-title":"J. Autom. Reason."},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Korni\u0142owicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: Formalization of the algebra of nominative data in Mizar. In: 2017 Federated Conference on Computer Science and Information Systems (2017, accepted)","DOI":"10.15439\/2017F301"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Bancerek, G., Byli\u0144ski, C., Grabowski, A., Korni\u0142owicz, A., Matuszewski, R., Naumowicz, A., P\u0105k, K., Urban, J.: Mizar: state-of-the-art and beyond. In: Intelligent Computer Mathematics \u2013 International Conference, CICM 2015, Proceedings, Washington, DC, USA, pp. 261\u2013279 (2015). http:\/\/dx.doi.org\/10.1007\/978-3-319-20615-8_17","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Grabowski, A., Korni\u0142owicz, A., Schwarzweller, C.: Equality in computer proof assistants. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2015 Federated Conference on Computer Science and Information Systems. Annals of Computer Science and Information Systems, vol. 5, pp. 45\u201354. IEEE (2015). http:\/\/dx.doi.org\/10.15439\/2015F229","DOI":"10.15439\/2015F229"},{"issue":"2","key":"16_CR20","first-page":"357","volume":"1","author":"C Byli\u0144ski","year":"1990","unstructured":"Byli\u0144ski, C.: Partial functions. Formaliz. Math. 1(2), 357\u2013367 (1990)","journal-title":"Formaliz. Math."},{"issue":"1","key":"16_CR21","first-page":"47","volume":"1","author":"C Byli\u0144ski","year":"1990","unstructured":"Byli\u0144ski, C.: Some basic properties of sets. Formaliz. Math. 1(1), 47\u201353 (1990)","journal-title":"Formaliz. Math."},{"issue":"4","key":"16_CR22","first-page":"485","volume":"5","author":"G Bancerek","year":"1996","unstructured":"Bancerek, G., Trybulec, A.: Miscellaneous facts about functions. Formaliz. Math. 5(4), 485\u2013492 (1996)","journal-title":"Formaliz. Math."}],"container-title":["Advances in Intelligent Systems and Computing","Information Systems Architecture and Technology: Proceedings of 38th International Conference on Information Systems Architecture and Technology \u2013 ISAT 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67229-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T00:58:34Z","timestamp":1570064314000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67229-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,7]]},"ISBN":["9783319672281","9783319672298"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67229-8_16","relation":{},"ISSN":["2194-5357","2194-5365"],"issn-type":[{"value":"2194-5357","type":"print"},{"value":"2194-5365","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,9,7]]}}}