Computer algebra (CA) systems and Proof Assistants (PAs) are two important kinds of programs which support complementary approaches to doing computer mathematics. The aim of my research is to combine the strengths of these two approaches with the ultimate goal of creating a uniform environment for computer mathematics.
Various approaches that combine PAs and CA have been proposed from both sides. First, to ensure correctness of the algorithms implemented in CA, the authors try certifying the algorithms externally or providing PA functionality in CA systems, an example of such approach is Theorema. Second, PAs implement more and more operations required for CA. HOL Light and Coq formalize certified versions of algorithms for computing Gröbner bases, Isabelle implements the HOL Computing Library, used for computations in the Flyspeck Project and there is ongoing work to create CAD in Coq. Next, there are frameworks for information exchange between CA and PAs. Finally, the recent advancements in verification of imperative programs allow certification of optimized imperative code.
In the project I developed / extended the following components
The prototype computer algebra system built on top of HOL Light. This architecture guarantees that one can be certain that the system will make no mistakes. All expressions in the system will have precise semantics, and the proof assistant will check the correctness of all simplifications according to this semantics. The system actually proves each simplification performed by the computer algebra system.