Authors: Micaela Mayero, David Delahaye
Title: A Quantifier Elimination Procedure over ACFs in Coq using Maple
Abstract: 
We present an interface between the Coq proof assistant and
the Maple computer algebra system. The aim of the interface is to
import, into Coq, computations over algebraic expressions carried out
by Maple. With this interface, it is either possible to perform pure
computations, which do not require any validation, or to perform
computations inside a proof, which have to be proved correct in Coq
(skeptical approach). In the particular case of algebraic expressions
over a field, the correctness proo fs are fully automatic and handled
by the Field tactic.
                                                                               
As an example, we describe a quantifier elimination procedure over
algebraically closed fields, where the interface has been extended to
deal with polynomial gcds. Thus, this shows that this interface may be
used to increase not only the power of computation of Coq but also its
automation.