Java_light is type-safe—definitely
The work
| Authors | Tobias Nipkow; David von Oheimb |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 1998 |
| Citekey | nipkow1998java |
Where it appeared
| Published in | Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '98) |
|---|---|
| Publisher | Association for Computing Machinery |
| Pages | 161--170 |
Identifiers
| DOI | 10.1145/268946.268960 |
|---|---|
| OpenAlex | W1989536180 |
Access
| Landing page | https://doi.org/10.1145/268946.268960 |
|---|---|
| Free full text | https://dl.acm.org/doi/pdf/10.1145/268946.268960 |
Abstract
Javalight 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.
A copy is held
pdf, 219.4 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-08-04 00:00 UTC |
| Approved by | a person 2026-08-10 14:34 UTC |
Filed under
Cite it as
@inproceedings{nipkow1998java,
title = {Java\_light is type-safe—definitely},
author = {Tobias Nipkow and David von Oheimb},
year = {1998},
booktitle = {Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '98)},
publisher = {Association for Computing Machinery},
pages = {161--170},
doi = {10.1145/268946.268960},
}
This record lives at https://refs.drheap.org/nipkow1998java/ and will keep doing so.