Kelly M. Hall, Phillip J. Windley: Simulating Microprocessors from Formal Specifications. TPHOLs 1992: 507-525