RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB
General information
Latest issue
Archive
Guidelines for authors
Submit a manuscript

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Program Systems: Theory and Applications:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Program Systems: Theory and Applications, 2018, Volume 9, Issue 4, Pages 509–560 (Mi ps327)  

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

Abstract: 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.

Funding Agency Grant Number
Russian Academy of Sciences - Federal Agency for Scientific Organizations AAAA-A16-116021760039-0


DOI: https://doi.org/10.25209/2079-3316-2018-9-4-509-560

Full text: PDF file (2231 kB)
References: PDF file   HTML file

UDC: 510.252, 004.432.42
MSC: Primary 03B35; Secondary 68T15, 03D60
Received: 03.07.2018
19.12.2018
Accepted: 30.12.2018

Citation: 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
\Bibitem{Mec18}
\by S.~D.~Mechveliani
\paper Constructing provable programs for arithmetic of natural numbers in binary representation
\jour Program Systems: Theory and Applications
\yr 2018
\vol 9
\issue 4
\pages 509--560
\mathnet{http://mi.mathnet.ru/ps327}
\crossref{https://doi.org/10.25209/2079-3316-2018-9-4-509-560}


Linking options:
  • http://mi.mathnet.ru/eng/ps327
  • http://mi.mathnet.ru/eng/ps/v9/i4/p509

    SHARE: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Program Systems: Theory and Applications
    Number of views:
    This page:38
    Full text:15
    References:4

     
    Contact us:
     Terms of Use  Registration  Logotypes © Steklov Mathematical Institute RAS, 2019