|
| From: | daly |
| Subject: | [Axiom-developer] Proving Axiom correct |
| Date: | Tue, 1 Dec 2015 07:51:59 -0500 (EST) |
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.
| [Prev in Thread] | Current Thread | [Next in Thread] |