TY - JOUR
T1 - A machine-checked model for a Java-like language, virtual machine, and compiler
AU - Klein, Gerwin
AU - Nipkow, Tobias
PY - 2006
Y1 - 2006
N2 - 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.
AB - 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.
KW - Java
KW - Operational semantics
KW - Theorem proving
UR - http://www.scopus.com/inward/record.url?scp=33747124759&partnerID=8YFLogxK
U2 - 10.1145/1146809.1146811
DO - 10.1145/1146809.1146811
M3 - Article
AN - SCOPUS:33747124759
SN - 0164-0925
VL - 28
SP - 619
EP - 695
JO - ACM Transactions on Programming Languages and Systems (TOPLAS)
JF - ACM Transactions on Programming Languages and Systems (TOPLAS)
IS - 4
ER -