Two More FREE softwares for Computational Algebra

A few weeks back we talked about 2 Free softwares for computational
algebra. Here we introduce two more. These were developed in France:

Coq: Coq is used for proving theorems in number theory.Coq is based on a logical
framework called "Calculus of Inductive Constructions" extended by a modular
development system for theories. It is a formal proof management system.
A proof done with Coq is mechanically checked by the machine. Coq allows, for
example, the definition of functions or predicates, stating mathematical
theorems and software specifications, developing interactively formal proofs of
these theorems as well as checking these proofs by a small certification "kernel".
For details and download, click here.

PARI/GP: PARI is a C library for computer algebra system and is designed for
fast computations in number theory (factorizations, algebraic number theory,
elliptic curves...) . It was developed by Henri Cohen and his co-workers at
Université Bordeaux I, France. It also contains a large number of other useful
functions to compute with mathematical entities such as matrices, polynomials,
power series, algebraic numbers, transcendental functions, etc.
GP is an easy-to-use interactive shell giving access to the PARI functions.
The package can be downloaded from here.