Type-preserving compilation of Featherweight Java
- 1 March 2002
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 24 (2) , 112-152
- https://doi.org/10.1145/514952.514954
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.Keywords
This publication has 8 references indexed in Scilit:
- An efficient class and object encodingPublished by Association for Computing Machinery (ACM) ,2000
- Comparing Object EncodingsInformation and Computation, 1999
- From system F to typed assembly languageACM Transactions on Programming Languages and Systems, 1999
- A Theory of ObjectsPublished by Springer Nature ,1996
- An interpretation of typed OOP in a language with stateHigher-Order and Symbolic Computation, 1995
- A paradigmatic object-oriented programming language: Design, static typing and semanticsJournal of Functional Programming, 1994
- Simple type-theoretic foundations for object-oriented programmingJournal of Functional Programming, 1994
- Abstract types have existential typeACM Transactions on Programming Languages and Systems, 1988