To make the paper self-contained, it starts with introductions to Isabelle/HOL and the art of embedding languages in theorem provers.
BibTeX:
@inproceedings{NipkowOP00, author={Tobias Nipkow and Oheimb, David von and Cornelia Pusch}, title={{$\mu$Java}: Embedding a Programming Language in a Theorem Prover}, booktitle={Foundations of Secure Computation. Proc.\ Int.\ Summer School Marktoberdorf 1999}, editor={F.L. Bauer and R. Steinbr\"uggen},publisher={IOS Press}, pages={117--144},year=2000}The corresponding Isabelle theories.