Java-light is Type-Safe - Definitely

Tobias Nipkow and David von Oheimb

Java-light is a large sequential sublanguage of Java. We formalize its abstract syntax, type system, well-formedness conditions, and an operational (evaluation) semantics. Based on this formalization, we can express and prove type soundness. All definitions and proofs have been done formally in the theorem prover Isabelle/HOL. Thus this paper demonstrates that machine-checking the design of non-trivial programming languages has become a reality.

dvi

BibTeX:

@inproceedings{Nipkow-Oheimb-POPL98,
author={Tobias Nipkow and David von Oheimb},
title={Java$_{{\ell}ight}$ is Type-Safe --- Definitely},
booktitle={Proc.\ 25th ACM Symp.\ Principles of Programming Languages},
publisher={ACM Press},year=1998,pages={161--170}}

The corresponding formalization as DVI or PS file (with graphical symbols) and as html pages (ASCII version).