|
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] |