The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Does anyone know of a Coq formalization of the semantics of the usual 
x86 instruction set, or a significant subset thereof?  I don't see 
anything linked from the contributions section of the Coq web site, and 
I've heard it said that such a formalization doesn't exist, but I 
thought I'd check here just in case.  I'd also be interested in 
formalizations for mostly-complete subsets of any "real" processor's 
instruction set, packaged as re-usable libraries.

P.S.: Thanks to everyone who replied to my last question about dependent 
types.  The advice I got enabled me to prove the theorem I was after.