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

Aldizkaria:
Lecture Notes in Computer Science

ISSN: 0302-9743

Argitalpen urtea: 2005

Alea: 3643 LNCS

Orrialdeak: 159-168

Mota: Artikulua

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

Beste argitalpen batzuk: Lecture Notes in Computer Science

Laburpena

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.