Coq: The world's best macro assembler?

Andrew Kennedy, Nick Benton, Jonas B. Jensen, Pierre-Evariste Dagand
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer] [url]

Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming
PPDP '13
Madrid, Spain
Association for Computing Machinery
New York, NY, USA
Pages 13-24
2013
Note(s): Coq theorem prover, ISA specification, Separation Logic
Papers: jensen:popl:2013