Program Systems: Theory and Applications, 2018, Volume 9, Issue 4, Pages 509–560
Mathematical Foundations of Programming
Constructing provable programs for arithmetic of natural numbers in binary representation
S. D. Mechveliani
Ailamazyan Program Systems Institute of Russian Academy of Sciences
Support for dependent types in a functional programming language Agda makes it
possible to include machine-checked proofs in the program. The problem of provable inclusion of
algorithms for arithmetic operations on natural numbers in binary representation is considered.
A library of evidentiary programs for “written calculation” algorithms, acting on bit lists
has been built. It contains machine-verifiable proofs of the required properties of the applied
algorithms, corrects and substantially supplements the Bin part of the lib-0.16
standard library of the Agda language. (In Russian).
Key words and phrases:
computer algebra, binary code arithmetic, provable programming, Agda language.
PDF file (2231 kB)
MSC: Primary 03B35; Secondary 68T15, 03D60
S. D. Mechveliani, “Constructing provable programs for arithmetic of natural numbers in binary representation”, Program Systems: Theory and Applications, 9:4 (2018), 509–560
Citation in format AMSBIB
\paper Constructing provable programs for arithmetic of natural numbers in binary representation
\jour Program Systems: Theory and Applications
Citing articles on Google Scholar:
Related articles on Google Scholar:
|Number of views:|