Publication
µJava: Embedding a Programming Language in a Theorem Prover
Foundations of Secure Computation
Author(s): Tobias Nipkow, David von Oheimb, Cornelia Pusch
Year: 2000
Publisher: IOS Press
Editor: Friedrich L. Bauer and Ralf Steinbrüggen
CR Classification: D.3.1, F.3.2
CR General Terms: Languages, Reliability, Theory, Verification
Keywords: Java, JVM, Bytecode Verifier, Embedding, Semantics, Type-Safety, Isabelle, HOL
Abstract:This paper introduces the subset µJava of Java,
essentially by omitting everything but classes.
The type system and semantics of this language
(and a corresponding abstract Machine µJVM)
are formalized in the theorem prover Isabelle/HOL.
Type safety both of µJava and the µJVM
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.
Available as compressed Postscript and PDF
BibTeX entry:
@inproceedings{NipkowOP00,
author = {Tobias Nipkow and David von Oheimb and Cornelia Pusch},
title = {{$\mu$Java}: Embedding a Programming Language in a Theorem Prover},
booktitle = {Foundations of Secure Computation},
series= {NATO Science Series F: Computer and Systems Sciences},
volume = {175},
year = {2000},
publisher = {IOS Press},
editor = {Friedrich L. Bauer and Ralf Steinbr{\"u}ggen},
abstract = {This paper introduces the subset $\mu$Java of Java,
essentially by omitting everything but classes.
The type system and semantics of this language
(and a corresponding abstract Machine $\mu$JVM)
are formalized in the theorem prover Isabelle/HOL.
Type safety both of $\mu$Java and the $\mu$JVM
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.},
CRClassification = {D.3.1, F.3.2},
CRGenTerms = {Languages, Reliability, Theory, Verification},
note = {\url{http://isabelle.in.tum.de/Bali/papers/MOD99.html}},
pages = {117--144}
}
Slides as gzipped PS file.
Isabelle sources