The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Type-Preserving Compilation of Featherweight Java

Last modified: Wed Aug 14 19:28:19 2002 GMT.

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.

Copyright © 1996-2024 The FLINT Group <flint at cs dot yale dot edu>
Yale University Department of Computer Science
Validate this page
colophon