The Coq-model of Atomic Entities in Formal Theories

Oleksandr Berezovskyi

Анотація


Atomic entities are significant basic elements of the logical modelling of subject areas of
software systems. Since modern software systems require guarantees of the correctness
of their functioning, formal logical models become a necessary tool for ensuring software
dependability. The article proposes a conceptual basis for modelling atomic entities, de-
veloped for using it for formal verification with The Coq Proof Assistant.

Повний текст:

PDF (English)

Посилання


The Coq Development Team. The Coq Proof Assistant. http://coq.inria.fr/

Naraschewski W., Nipkow T. Isabelle/HOL: a proof assistant for higher-order logic.
http://www.cl.cam.ac.uk/research/hvg/Isabelle/

The Agda Team. The Agda Wiki. https://wiki.portal.chalmers.se/agda/Main/HomePage

Chlipala A. Certified Programming with Dependent Types: A Pragmatic Introduction to
the Coq Proof Assistant. – The MIT Press, 2022.

Hoare C.A.R. An axiomatic basis for computer programming. CACM. 12 (10) 1969. –
Pp. 576–580.

Hindley J.R., Seldin J.P. Lambda-Calculus and Combinators: An Introduction. – Cambridge University Press, 2008, 2ed.




DOI: http://dx.doi.org/10.30970/vam.2023.31.11967

Посилання

  • Поки немає зовнішніх посилань.