Java_light is type-safe—definitely
The work
| Title | Java_light is type-safe—definitely |
|---|---|
| Authors | Tobias Nipkow; David von Oheimb |
| Type | conference paper |
| 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.
Copy held
| Kind | PDF, 224.6 kB |
|---|---|
| Retrieved | 2026-08-10 |
| Held | local, for personal reference |
| Where it came from | https://david.von-oheimb.de/cs/papers/POPL98.pdf |
Where this came from
| How it got here | the agent went looking · found via openalex |
|---|---|
| First seen | 2026-08-04 |
| Record | reviewed by a person |
| Approved | 2026-08-10 |
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)},
pages = {161--170},
publisher = {Association for Computing Machinery},
doi = {10.1145/268946.268960},
url = {https://dl.acm.org/doi/pdf/10.1145/268946.268960},
}
This record lives at https://refs.drheap.org/nipkow1998java/ and will keep doing so.