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.
ACM page
© 1998 by ACM, Inc.
Authors' ps
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}}