I looked again at Hansen's stuff.
It is apparently possible to call from C into ECL as a library,
but you are going to have trouble with memory allocation.
You either leave any pointer stuff on the stack or you have to make some
special deal to protect data.
My view is that the ECL Boehm conservative garbage collection idea is
cute, but not anything I would like to
rely on for good performance over some span of time.
It is really simple enough to initialize a lump of code that includes
lisp, and then have that lump invoke at the startup, a call to
a C program, call it X, that appears to be "in charge". X can now
allocate memory from the Lisp heap, and
perhaps elsewhere. It can call CONS. It can pass around Lisp data
without re-copying it, or translating
or parsing etc. If you don't have some Lisp initialization before
calling C, you are probably quite limited in what
you can do.
This much sophistication is probably unnecessary for Nathan's application.
There is a moderate literature on proving the equivalence of algebraic
expressions by various means, including
hashcoding, used by William Martin (1971), Gaston Gonnet (in Maple).
Simplification works sometimes, and may work for everything you need,
but it is not by any means a theorem
that if you have two equivalent expressions, A, B, that simplify(A-B)
will be zero.
It is, in fact, a theorem that such a simplification program cannot
exist. (Daniel Richardson, 1968)
RJF