[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.
Tim
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
>