A type preserving translation of ickle into Java
Davide Ancona, C. Anderson, Ferruccio Damiani, Sophia Drossopoulou, Paola Giannini, Elena Zucca · Electronic Notes in Theoretical Computer Science · 2002
We present a translation from F ickle (a Java-like language allowing objects that can change their class at run-time) into plain Java. The translation, which maps any F ickle class into a Java class, is driven by an invariant that relates a F ickle object to its Java counterpart. The translation, which is proven to preserve both the static and the dynamic semantics of the language, is an enhanced version of a previous proposal by the same authors.