Coq: The world's best macro assembler? http://research.microsoft.com/en-us/um/people/nick/coqasm.pdf
This describes a Coq formalization of a subset of the x86 architecture. So now we have a reasonably complete stack of proof technology. _______________________________________________ Axiom-developer mailing list [email protected] https://lists.nongnu.org/mailman/listinfo/axiom-developer
