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.

- Publications at Calculemus 2007, 2008, and 2011.
- Download version 4 (requires Hol Light from January 2010).
- View example interaction log.

- Included in Isabelle, since 2011
- Publication at SAC 2011

- Included in Nominal 2, since 2012
- Publication at CPP 2011

- Publication at ADG 2012