root <[EMAIL PROTECTED]> writes: | Functional Pearl, A Type-correct, stack-safe, provably correct | expression compiler in Epigram. | http://www.cs.nott.ac.uk/~jjw/papers/Compiler_Pearl/Compiler_Pearl.pdf | | | I've mentioned before that it is a long term goal of Axiom to | enhance the compiler to prove properties of Categores and Domains.
We need a clear formulation of the type system for that. Adn we also need a clear grammar. | This is of interest because of that goal. I'd like to be able to | do things like decorate the Categories and Domains with mathematical | axioms (e.g. Group) and prove properties like commutative rather | than just assert them. Funny, you should mention that. In our design for "C++ concepts", we have provision for that -- though it is not enforced in the typpe system directtly, but can be used for auxiliary tools. -- Gaby _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
