The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Daniel, you may be interested by using/contributing to 
http://focalize.inria.fr/ . Regards, Frédéric.

Le 23/05/2014 20:21, Daniel Schepler a écrit :
> I've toyed with the idea of starting a project for a formally verified
> Computer Algebra System.  One of my high-level design goals would be
> to make all the functionality accessible directly through Coq, in
> addition to the more conventional "command line" type interface, in
> order to be able to extract "proofs by reflection".
>
> I don't know that much about how existing CASes are structured,
> though, so I don't know how much I could contribute to such a project.
>   We could hopefully leverage some of the existing open source CAS
> projects like Axiom and Maxima for ideas, though I've only really used
> Maxima myself, and that not very seriously.