Type-Preserving Compilation of Featherweight Java

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 v-tables 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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2005
Accession Number
ADA436480

Entities

People

  • Christopher League
  • Valery Trifonov
  • Zhong Shao

Organizations

  • Yale University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Assembly Languages
  • Coding
  • Compilers
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Construction
  • Java Programming Language
  • Language
  • New York
  • Object Code
  • Object Oriented Programming
  • Object-Oriented Programming Language
  • Programming Languages
  • Standards

Fields of Study

  • Computer science

Readers

  • Computer Programming and Software Development.
  • Database Systems and Applications