Jinja: Towards a Comprehensive Formal Semantics for a
Java-like Language
Jinja is a Java-like programming language with a formal semantics designed to
exhibit core features of Java. It is a compromise between realism of the
language and tractability and clarity of the formal semantics. A big and a
small step operational semantics are defined and shown equivalent. A type
system and a definite initialization analysis are defined and type safety of
the small step semantics is shown. The whole development has been carried out
in the theorem prover Isabelle/HOL.
pdf
BibTeX:
@inproceedings{Nipkow-MOD2003,author={Tobias Nipkow},
title={Jinja: Towards a Comprehensive Formal Semantics for a
{J}ava-like Language},
booktitle={Proof Technology and Computation},
publisher={IOS Press},editor={H. Schwichtenberg and K. Spies},
year=2006,pages={247--277}}
For a very much extended and revised version, including the virtual machine
and a compiler, see HERE