A machine-checked model for a Java-like language, virtual machine, and compiler

The work

AuthorsGerwin Klein; Tobias Nipkow
Editors
Typearticle
Year2006
Citekeyklein2006machinechecked

Where it appeared

Published inACM Transactions on Programming Languages and Systems
PublisherAssociation for Computing Machinery
Volume28
Issue4
Pages619--695

Identifiers

DOI10.1145/1146809.1146811
OpenAlexW2052735108

Access

Landing pagehttps://doi.org/10.1145/1146809.1146811
Free full texthttps://dl.acm.org/doi/pdf/10.1145/1146809.1146811

Related

Distinct fromklein2018formally

Abstract

We introduce Jinja, a Java-like programming language with a formal semantics designed to exhibit core features of the Java language architecture. Jinja is a compromise between the realism of the language and the tractability and clarity of its formal semantics. The following aspects are formalised: a big and a small step operational semantics for Jinja and a proof of their equivalence, a type system and a definite initialisation analysis, a type safety proof of the small step semantics, a virtual machine (JVM), its operational semantics and its type system, a type safety proof for the JVM; a bytecode verifier, that is, a data flow analyser for the JVM, a correctness proof of the bytecode verifier with respect to the type system, and a compiler and a proof that it preserves semantics and well-typedness. The emphasis of this work is not on particular language features but on providing a unified model of the source language, the virtual machine, and the compiler. The whole development has been carried out in the theorem prover Isabelle/HOL.

A copy is held

pdf, 620.4 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via openalex
Added2026-08-04 00:00 UTC
Approved bya person 2026-08-10 14:34 UTC

Filed under

gerwinklein the-copy-is-not-the-work toplas verifying-real-java

Cite it as

@article{klein2006machinechecked,
  title        = {A machine-checked model for a Java-like language, virtual machine, and compiler},
  author       = {Gerwin Klein and Tobias Nipkow},
  year         = {2006},
  journal      = {ACM Transactions on Programming Languages and Systems},
  publisher    = {Association for Computing Machinery},
  volume       = {28},
  number       = {4},
  pages        = {619--695},
  doi          = {10.1145/1146809.1146811},
}

This record lives at https://refs.drheap.org/klein2006machinechecked/ and will keep doing so.