General theory and tools for proving algorithms in nominative data systems
From MaRDI portal
Publication:6592314
DOI10.2478/FORMA-2020-0024zbMATH Open1543.6842MaRDI QIDQ6592314
Publication date: 26 August 2024
Published in: Formalized Mathematics (Search for Journal in Brave)
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)
Cites Work
- Title not available (Why is that?)
- Four decades of {\textsc{Mizar}}. Foreword
- Proving properties of programs on hierarchical nominative data
- Implementation of the composition-nominative approach to program formalization in Mizar
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Simple-named complex-valued nominative data -- definition and basic operations
- Kleene algebra of partial predicates
- On algebras of algorithms and specifications over uninterpreted data
- On an algorithmic algebra over simple-named complex-valued nominative data
- An inference system of an extension of Floyd-Hoare logic for partial predicates
- Partial correctness of GCD algorithm
- Partial correctness of a factorial algorithm
- Partial correctness of a power algorithm
- An axiomatic basis for computer programming
Related Items (1)
This page was built for publication: General theory and tools for proving algorithms in nominative data systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6592314)
