Top

Programming and Computer Software

Published in:

01-03-2020

On a Machine-Checked Proof for Fraction Arithmetic over a GCD Domain

Author: S. D. Meshveliani

Published in: Programming and Computer Software | Issue 2/2020

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

In this paper, we describe design principles for certified programs of fraction arithmetic over any domain with the greatest common divisor (GCD) function. This is a small part of the DoCon-A library of certified programs, which is designed by the author of this paper. In this system, programs include definitions of the corresponding mathematical notions and proofs for the main properties of the methods implemented. These proofs are checked by the compiler. A purely functional programming language Agda, which supports dependent types, is used. A technique to generate formal machine-checked proofs for a certain optimized method of fraction addition is described.

previous article Algorithm for Constructing an Analogue of the Binet Formula

next article Construction of a Periodic Solution to the Equations of Motion of Generalized Atwood’s Machine using Computer Algebra

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Meshveliani, S.D., On dependent types and intuitionism in programming mathematics, in Electronic library of Cornel University. http://arxiv.org/find/all:+Mechveliani/0/1/0/all/0/1 (2017).

Meshveliani, S.D., DoCon-A: A library of provable programs for computer algebra, 2015–2018. http://www.botik.ru/pub/local/Mechveliani/docon-A.

Mechveliani, S.D., Computer algebra with Haskell: Applying functional-categorial-'lazy' programming, Proc. Int. Workshop CAAP, Gerdt, V.P., Ed., Dubna, 2001, pp. 203–211.

Norell, U., Dependently typed programming in Agda, Adv. Funct. Program.,Lect. Notes Comput. Sci., Springer, 2008, vol. 5832, pp. 230–266.MATH

Wikipedia, Agda. http://wiki.portal.chalmers.se/agda/pmwiki.php.

Curry, H.B. and Feys, R., Combinatory Logic, Amsterdam, 1958, vol. 1.MATH

Howard, W.A., The formulae-as-types notion of construction, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Boston: Academic, 1980, pp. 479–490.

Markov, A.A., On constructive mathematics, Tr. Mat. Inst.im.V. A. Steklova, 1962, vol. 67, pp. 8–14.

Martin-Loef, P., Intuitionistic Type Theory, Bibliopolis, 1984.

10.

van der Waerden, B.L., Algebra, Springer, 1971, vol. 1.MATH

11.

Knuth, D.E., The Art of Computer Programming, Addison-Wesley, 1969, vol. 2.MATH

12.

Jenks, R.D., Sutor, R.S., et al., Axiom: The Scientific Computation System, Springer, 1992.MATH

13.

Chlipala, A., Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant, MIT Press, 2013. http://adam.chlipala.net/cpdt.

14.

de Moura, L., Kong, S., Avigad, J., van Doorn, F., and von Raumer, J., The Lean theorem prover, Proc. 25th Int. Conf. Automated Deduction (CADE), Berlin, 2015. https://leanprover.github.io/papers/system.pdf.

Title: On a Machine-Checked Proof for Fraction Arithmetic over a GCD Domain
Author: S. D. Meshveliani
Publication date: 01-03-2020
Publisher: Pleiades Publishing
Published in: Programming and Computer Software / Issue 2/2020
Print ISSN: 0361-7688
Electronic ISSN: 1608-3261
DOI: https://doi.org/10.1134/S0361768820020073

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Technik"

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Other articles of this Issue 2/2020

Procedures for Searching Laurent and Regular Solutions of Linear Differential Equations with the Coefficients in the Form of Truncated Power Series

Bifurcations of Periodic Solutions of a Hamiltonian System with a Discrete Symmetry Group

Construction of a Periodic Solution to the Equations of Motion of Generalized Atwood’s Machine using Computer Algebra

Normalization of a Periodic Hamiltonian System

Algorithm for Constructing an Analogue of the Binet Formula

Computation of Involutive and Gröbner Bases Using the Tableau Representation of Polynomials

Premium Partner