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. 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. Tim _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
