[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Axiom musings...

From: Tim Daly
Subject: Re: Axiom musings...
Date: Tue, 26 Nov 2019 04:08:26 -0500

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.


On 11/26/19, Tim Daly <address@hidden> 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

reply via email to

[Prev in Thread] Current Thread [Next in Thread]