Jinja: Towards a Comprehensive Formal Semantics for a Java-like Language

Tobias Nipkow

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.



@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},
For a very much extended and revised version, including the virtual machine and a compiler, see HERE