Re: Axiom musings...

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" 
http://www.cas.mcmaster.ca/~carette/publications/tpcj.pdf [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 
https://alhassy.github.io/next-700-module-systems/prototype/package-former.html 
(source at https://github.com/alhassy/next-700-module-systems). It is 
literate source.

The old prototype was hard to find - it is now at 
https://github.com/JacquesCarette/MathScheme.

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" 
(https://alhassy.github.io/next-700-module-systems/papers/gpce19_a_language_feature_to_unbundle_data_at_will.pdf) 
is also relevant, as it solves a problem with parametrized theories 
(parametrized Categories in Axiom terminology) that all current systems 
suffer from.

Jacques

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.
>
> Tim
>
>
> On 11/26/19, Tim Daly <[email protected]> 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 <[email protected]> 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
>>>