[Axiom-developer] Axiom + Coq?

[C Y]

In the paper "On the way to certify Computer Algebra Systems" by S.
Boulm'e, T. Hardin, D. Hirschkoff, V. M'enissier-Morain, and R. Rioboo
the following description is made: 

"Within a previous project, we have tried to interface Axiom and the
Coq proof assistant, with the aim of proving some properties of Axiom
programs[1]. A prototype has been done, consisting firstly in
interfaces between libraries of Axiom (basic, sets, ordered sets, . . .
, groups) with the corresponding theories in Coq, and secondly, in a
compiler from Axiom functions to their specifications in Coq. The
emphasis has been put on the compilation of the hierarchy of categories
and domains; as far of the actual code is concerned, only the
imperative kernel was considered. The main outcome of this previous
work was that such a task should rather be attacked using a programming
language whose semantics is fully understood (and, possibly,
formalized). Indeed, for example, some diAEculties arose in modeling
multiple inheritance within Axiom programs, mostly because we could not
coin a precise semantics of this (quite intricate) programming
construct. Overall, it seems that in some sense the Axiom programmer
has too much freedom for his implementation task, and can hence design
programs that are quite diAEcult, if not impossible, to certify. In
particular, the management of definitions by default, as well as
definition overriding, seems diAEcult to handle when it comes to
guarantee a reasonable form of coherence within the "proof" part of a
development."

The reference is apparently to this:

1. Guillaume Alexandre. D'Axiom `a Zermelo. Th`ese de l'universit'e
Paris 6, February 1998. 

Does anyone know if this work is available anywhere?  (An English
translation would be even better :-) This sounds like it pursued almost
exactly what we need, and the results, if available, would be extremely
interesting to review or perhaps even build off of.

Cheers,
CY


                
__________________________________ 
Yahoo! Mail - PC Magazine Editors' Choice 2005 
http://mail.yahoo.com