Experience with embedding hardware description languages in HOL

Richard Boulton, Andrew Gordon, Michael J. C. Gordon, John Harrison, John Herbert, John Van Tassel
[Google Scholar] [DBLP] [Citeseer] [url]

Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience
IFIP Transactions A: Computer Science and Technology, volume A-10
Nijmegen, The Netherlands
Pages 129-156
Note(s): HOL theorem prover, embedding