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