Lifted Java: A Minimal Calculus for Translation Polymorphism

Abstract

To support roles and similar notions involving multiple views on an object, languages like Object Teams and CaesarJ include mechanisms known as lifting and lowering. These mechanisms connect pairs of objects of otherwise unrelated types, and enable programmers to consider such a pair almost as a single object which has both types. In the terminology of Object Teams this is called translation polymorphism. In both Object Teams and CaesarJ the type system of the Java programming language has been extended to support this through the use of advanced language features. The type soundness of translation polymorphism has so far only been proven in a simple special case. This paper presents a simple model that extends Featherweight Java with a general semantics that captures the core operations of translation polymorphism, providing an entire language design space for languages with translation polymorphism. Type soundness is proven for every language in this language design space, and mechanization of the proof in Coq shows that the proof is accurate and complete.

Keywords

Formal foundations, language design, lifting/lowering, Translation Polymorphism, type systems

Cite as:

Matthias Diehn Ingesman, Erik Ernst, “Lifted Java: A Minimal Calculus for Translation Polymorphism”, Journal of Object Technology, Volume 11, no. 1 (April 2012), pp. 2:1-23, doi:10.5381/jot.2012.11.1.a2.