Re: Axiom musings...

[Tim Daly]

The new Sane compiler is also being tested with the Fricas
algebra code. The compiler knows about the language but
does not depend on the algebra library (so far). It should be
possible, by design, to load different algebra towers.

In particular, one idea is to support the "tiny theories"
algebra from Carette and Farmer. This would allow much
finer grain separation of algebra and axioms.

This "flexible algebra" design would allow things like the
Lean theorem prover effort in a more natural style.

Tim


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