Proving Translation and Reduction Semantics Equivalent for Java Simple Closures: Extended Version

\Lname\ is a minimal core calculus that extends Featherweight (generic) Java, \FGJ, with lambda expressions. It has been used to study properties of Simple Closure in Java, including type safety and the abstraction property. Its formalization is based on a reduction semantics and a typing system that extend those of \FGJ. ${\cal F}$ is a source-to-source, translation rule system from Java 1.5 extended with lambda expressions back to ordinary Java 1.5. It has been introduced to study implementation features of closures in Java, including assignment of non local variables and relations with anonymous class objects. In this paper we prove that the two semantics commute.