The current design and code base (in bookvol15) supports
multiple back ends. One will clearly be a common lisp.
Another possible design choice is to target the GNU
GCC intermediate representation, making Axiom "just
another front-end language" supported by GCC.
The current intermediate
Jason Gross and Adam Chlipala ("Parsing Parses") developed
a dependently typed general parser for context free grammar
in Coq.
They used the parser to prove its own completeness.
Unfortunately Spad is not a context-free grammar.
But it is an intersting thought exercise to consider
an "Axiom on
