A Reflective Functional Language for Hardware Design and Theorem Proving - Grundy, J; Melham, T; O'Leary, J (Programming Research Group‚ Oxford University Computing Laboratory, 2003)