A type preserving translation of Fickle into Java