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 representation does not (yet)
make any decision about the runtime implementation.
Tim
On 11/26/19, Tim Daly <axiom...@gmail.com> wrote:
> 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 Coq" implementation.
>
> Tim
>
