Authors
Christopher League
Zhong Shao
Valery Trifonov
Abstract
We present an efficient encoding of core Java constructs in a simple,
implementable typed intermediate language. The encoding, after type
erasure, has the same operational behavior as a standard
implementation using vtables and self-application for method
invocation. Classes inherit super-class methods with no overhead. We
support mutually recursive classes while preserving separate
compilation. Our strategy extends naturally to a significant subset
of Java, including interfaces and privacy. The formal translation
using Featherweight Java allows comprehensible type-preservation
proofs and serves as a starting point for extending the translation to
new features. Our work provides a foundation for supporting
certifying compilation of Java-like class-based languages in a
type-theoretic framework.
Published
- To appear in ACM Transactions on Programming Languages and Systems
(TOPLAS), 24(2), pages 112-152, March 2002.