> Such a collection would be indeed desirable as there is none - at least > not comprehensive enough. Most favourable of course would be a library > of formally verified algorithms like CoqEAL
I have an initial effort on a wider bibliography http://axiom-developer.org/axiom-website/bookvolbib.pdf which I have started to lay out by year http://axiom-developer.org/axiom-website/lattice.html Hover over the numbers for the title. The citation is in the source code for the web page. I'm not sure what a good way to show the information might be. If you hover over a number should it also show lines to the papers it references? That info is in the page source but not used yet. I am not the best person to do user interface design, as you can see. Ideally clicking on a link would open the actual paper. Half of the standards problem is the citation lattice, shown above. This will be foundational information for when and where an algorithm first arose. It will also show improvements and their history. Densely referenced nodes are certainly important. The other half of the standards problem is what is actually implemented in existing systems. I'm instrumenting Axiom to give a trace of the algorithms used in the solution of an input. This will allow me to build up a tower of the algorithms. Then I need to relate the implementations to the published papers. A similar instrumentation of Maxima would show what algorithms are implemented there. The third half of the standards problem is getting it supported :-) We're 40+ years into computational mathematics. This needs to be done. > (http://www.maximedenes.fr/content/coqeal-coq-effective-algebra-library) > taking advantage of the relatively new SSReflect (tutorial -> > http://hal.archives-ouvertes.fr/docs/00/40/77/78/PDF/RT-367.pdf). > The implementation of Bourbaki's "Elements of Mathematics" by Jose Grimm > (http://www-sop.inria.fr/marelle/gaia/index.html) demonstrates in an > impressive way the feasibility to create such a mathematical firm > collection of algorithms. > Regarding 'pseudocode' it might be better (imho) to use the language of > one of the available proof assistants of which Coq is only one suitable > to do the task (http://en.wikipedia.org/wiki/Proof_assistant). Although > I have no profund knowledge of the others (than Coq and Isabelle), it > would be surely preferable to choose one that is capable of 'code > generation' as it might be easier (one day ;) than expected to write a > generator for spad/aldor. I'm not sure what the "pseudocode" might be but I can't actually advocate writing Spad code. The standards idea is supposed to be somewhat more general, not a self-serving effort. I am looking at COQ for a different reason, namely that I'm trying to prove an Axiom algorithm correct. See http://axiom-developer.org/axiom-website/bookvol13.pdf for the place-holder document. I started with the euclidean algorithm. There are "layers" of the problem so I'm looking at COQ for a Spad-to-Lisp proof, ACL2 for a Lisp-to-C proof, and my own research on Conditional Concurrent Assignments for C-to-Intel semantics. This is a "thin-thread" approach, trying to take one algorithm all the way from Spad to the machine. It would be really useful if the standard algorithms could be proven correct. Code generation from COQ would be ideal. Tim _______________________________________________ Axiom-developer mailing list [email protected] https://lists.nongnu.org/mailman/listinfo/axiom-developer
