Speaker
Dr
Sergei Meshveliani
(Program systems institute, Pereslavl-Zalessky, Russia)
Description
It is described a certain provable program for a generic arithmetic
of fractions. This is a small part of the project DoCon-A of provable
programs for a computer algebra library. In this system, functional
programs for known algebraic methods are written together with proofs, and proofs are automatically checked by the compiler (see the Coq and Agda systems). The used language (Agda) is purely functional and includes the feature of dependent types. This paper describes provable programming of arithmetic of fractions over arbitrary ring with gcd.
Short biography note
The author is a senior researcher in Program Systems Institute of Russian academy of sciences. He is the author of computer algebra systems DoCon and DoCon-A. His research is in automatization of symbolic computation and proofs.
Primary author
Dr
Sergei Meshveliani
(Program systems institute, Pereslavl-Zalessky, Russia)
