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

Revista:
Lecture Notes in Computer Science

ISSN: 0302-9743

Año de publicación: 2005

Volumen: 3643 LNCS

Páginas: 159-168

Tipo: Artículo

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

Otras publicaciones en: Lecture Notes in Computer Science

Resumen

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.