Proving Translation and Reduction Semantics Equivalent for Java Simple Closures

FGCJ 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. F is a source-tosource, 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.