Paper on semantics of Java-like language

The following paper may be of interest to readers of the types mailing
list. Feedback is very welcome.


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.