Extracting Computer Algebra programs from statements

  1. Aransay, J. 1
  2. Ballarin, C. 2
  3. Rubio, J. 1
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

  2. 2 Technical University Munich
    info

    Technical University Munich

    Múnich, Alemania

    ROR https://ror.org/02kkvpp62

Journal:
Lecture Notes in Computer Science

ISSN: 0302-9743

Year of publication: 2005

Volume: 3643 LNCS

Pages: 159-168

Type: Article

DOI: 10.1007/11556985_21 SCOPUS: 2-s2.0-33646010929 WoS: WOS:000233888200021 GOOGLE SCHOLAR

More publications in: Lecture Notes in Computer Science

Abstract

In this paper, an approach to synthesize correct programs from specifications is presented. The idea is to extract code from definitions appearing in statements which have been mechanically proved with the help of a proof assistant. This approach has been found when proving the correctness of certain Computer Algebra programs (for Algebraic Topology) by using the Isabelle proof assistant. To ease the understanding of our techniques, they are illustrated by means of examples in elementary arithmetic. © Springer-Verlag Berlin Heidelberg 2005.