Extracting Computer Algebra programs from statements
- Aransay, J. 1
- Ballarin, C. 2
- Rubio, J. 1
-
1
Universidad de La Rioja
info
-
2
Technical University Munich
info
ISSN: 0302-9743
Argitalpen urtea: 2005
Alea: 3643 LNCS
Orrialdeak: 159-168
Mota: Artikulua
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.