#### Tobias Nipkow, David von Oheimb, Cornelia Pusch

This paper introduces the subset microJava of Java, essentially by omitting everything but classes. The type system and semantics of this language (and a corresponding abstract Machine microJVM) are formalized in the theorem prover Isabelle/HOL. Type safety both of microJava and the microJVM are mechanically verified.

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.