[Top][All Lists]

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

Re: Axiom musings...

From: Jacques Carette
Subject: Re: Axiom musings...
Date: Thu, 28 Nov 2019 16:18:33 -0500
User-agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:60.0) Gecko/20100101 Thunderbird/60.9.1

The underlying technology to use for building such an algebra library is documented in the paper " Building on the Diamonds between Theories: Theory Presentation Combinators" [which will also be on the arxiv by Monday, and has been submitted to a journal].

There is a rather full-fledged prototype, very well documented at (source at It is literate source.

The old prototype was hard to find - it is now at

There is also a third prototype in the MMT system, but it does not quite function properly today, it is under repair.

The paper "A Language Feature to Unbundle Data at Will" ( is also relevant, as it solves a problem with parametrized theories (parametrized Categories in Axiom terminology) that all current systems suffer from.


On 2019-11-27 11:47 p.m., Tim Daly wrote:
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.


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.


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.


reply via email to

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