Publication

Java_light is Type-Safe -- Definitely

Proc. 25th ACM Symp. Principles of Programming Languages

Author(s): Tobias Nipkow and David von Oheimb
Year: 1998
Publisher: ACM Press, New York
Editor:
CR Classification: F.3.3, D.3.2, F.3.1, D.3.1
CR General Terms: Design, Languages, Reliability, Verification
Keywords: Java, Semantics, Theorem Proving, Type-Safety, Isabelle
Abstract: 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.

Preprint version available as gzipped PS file and PDF file.
Slides as gzipped DVI file.
The corresponding formalization as DVI or PS file (with graphical symbols) and as html pages (ASCII version)

Official version as ACM Digital Libray entry (PDF file)

BibTeX Entry:

@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}, year = {1998}, publisher = {ACM Press, New York}, editor = {}, note = {\url{http://isabelle.in.tum.de/Bali/papers/POPL98.html}}, abstract = {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.}, CRClassification = {F.3.3, D.3.2, F.3.1, D.3.1}, CRGenTerms = {Design, Languages, Security, Verification}, pages={161--170} }