microJava: Embedding a Programming Language in a Theorem Prover

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.

dvi

ps

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.