A machine-checked model for a Java-like language, virtual machine, and compiler
The work
| Title | A machine-checked model for a Java-like language, virtual machine, and compiler |
|---|---|
| Authors | Gerwin Klein; Tobias Nipkow |
| Type | article |
| Year | 2006 |
| Citekey | klein2006machinechecked |
Where it appeared
| Published in | ACM Transactions on Programming Languages and Systems |
|---|---|
| Publisher | Association for Computing Machinery |
| Volume | 28 |
| Issue | 4 |
| Pages | 619--695 |
Identifiers
| DOI | 10.1145/1146809.1146811 |
|---|---|
| OpenAlex | W2052735108 |
Access
| Landing page | https://doi.org/10.1145/1146809.1146811 |
|---|---|
| Free full text | https://dl.acm.org/doi/pdf/10.1145/1146809.1146811 |
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.
Copy held
| Kind | PDF, 635.3 kB |
|---|---|
| Retrieved | 2026-08-10 |
| Held | local, for personal reference |
| Where it came from | https://web.archive.org/web/20221005193648id_/https://www21.in.tum.de/~nipkow/pubs/Jinja/jinja.pdf |
Where this came from
| How it got here | the agent went looking · found via openalex |
|---|---|
| First seen | 2026-08-04 |
| Record | reviewed by a person |
| Approved | 2026-08-10 |
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},
volume = {28},
number = {4},
pages = {619--695},
publisher = {Association for Computing Machinery},
doi = {10.1145/1146809.1146811},
url = {https://dl.acm.org/doi/pdf/10.1145/1146809.1146811},
}
This record lives at https://refs.drheap.org/klein2006machinechecked/ and will keep doing so.