Dealing with algebraic expressions over a field in Coq using Maple

AbstractWe describe an interface between the Coq proof assistant and the Maple symbolic computation system, which mainly consists in importing, in Coq, Maple computations regarding algebraic expressions over fields. These can either be pure computations, which do not require any validation, or computations used during proofs, which must be proved (to be correct) within Coq. These correctness proofs are completed automatically thanks to the tactic Field, which deals with equalities over fields. This tactic, which may generate side conditions (regarding the denominators) that must be proved by the user, has been implemented in a reflexive way, which ensures both efficiency and certification. The implementation of this interface is quite light and can be very easily extended to get other Maple functions (in addition to the four functions we have imported and used in the examples given here)