nach oben

Programming and Computer Software

Erschienen in:

01.03.2020

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

verfasst von: S. D. Meshveliani

Erschienen in: Programming and Computer Software | Ausgabe 2/2020

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Vorheriger Artikel Algorithm for Constructing an Analogue of the Binet Formula

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

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

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.

Titel: On a Machine-Checked Proof for Fraction Arithmetic over a GCD Domain
verfasst von: S. D. Meshveliani
Publikationsdatum: 01.03.2020
Verlag: Pleiades Publishing
Erschienen in: Programming and Computer Software / Ausgabe 2/2020
Print ISSN: 0361-7688
Elektronische ISSN: 1608-3261
DOI: https://doi.org/10.1134/S0361768820020073

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Technik"

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 2/2020

Minimal Representations and Algebraic Relations for Single Nested Products

Differential Geometry and Mechanics: A Source for Computer Algebra Problems

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

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

Normalization of a Periodic Hamiltonian System

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

Premium Partner