Paper on semantics of Java-like language

• To: types@cis.upenn.edu
• Subject: Paper on semantics of Java-like language
• From: nipkow@in.tum.de
• Date: Mon, 20 Oct 2003 11:48:20 +0200 (MEST)

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

Tobias


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.

http://www.in.tum.de/~nipkow/pubs/MOD2003.html

• Prev: RE: mechanical proof checkers for type soundness?
• Next: Concur 2004 Preliminary Announcement
• Index(es):
  • Main
  • Thread