This project originated  from the idea of extending Java, based on the OO paradigm, with higher order mechanisms to enhance its expressivity and code reusability, in order to facilitate writing programs which are correct, well suited to the applications and can be easily adapted for a different use.

In 2004, \cite {bellia2004} through a case study we compare the expressivity of five different programs, all based on the OO programming paradigm but using also higher order mechanisms (mainly in the form of methods with higher order functionalities), all solving the same problem. Three programs are written in Java, one is written in J++ and the last one is written in Pizza.  As far as the higher order mechanisms are concerned, the first two programs in Java use reflection, the third one uses anonymous classes, the J++ program uses delegates and the Pizza program uses function abstractions (closures).

The result of the comparison led to identify three possible mechanisms to add to Java to extend it with higher order: higher order methods, method extraction and closures.

In \cite{bellia2005} the integration of such mechanisms in an OO paradigm is studied, through the extension of the $\zeta$-calcolo \cite{abadi96}. The new calculus $\zeta_x$-calculus provides for such mechanisms the reduction semantics and the typing rules and prove calculus confluence, subtyping, subtyping controvariance, subject reductions hence type soundness.

If the problem of the integration of HO mechanisms in an OO language can be considered positively solved, the problem of how this can be accomplished in Java is still open. As a matter of fact, the language Java has an implementation based on a mixture of compilation and interpretation. At the top level of the implementation process is a compiler that translates Java programs into Java bytecodes for the Java virtual machine, JVM. The machine is a collection of structures for processing bytecodes and has been designed to be defined once and to have as many different implementations as the different platforms that run Java programs.

This implementation ensures retargetability of Java compilers and high portability of the Java object code. In extending Java with new mechanisms is good practice to plan to preserve such appealing features of its implementation.

In Bellia2007  we began to study the design of HO mechanisms especially tailored for Java and its peculiar implementation, defining the structure of m_parameters as a form of higher order methods for Java. Bellia2007, Bellia2008 provide  the syntactic extensions to Java grammar to pass methods as parameters to other methods. A formal semantics is also defined and examples that show the use of the mechanism are shown. The expressivity is discussed by comparing programs that use such a mechanism with programs that compute in an almost equivalent way but are written in ordinary Java.

·      One of the most remarkable aspects of our study is the formal semantics which is defined in the form of a translation semantics. This kind of semantics maps programs of the extended language into programs of ordinary Java  and has three main benefits.

·      It defines the meanings of the new constructs in terms of the well known constructs of Java, without the introduction of the semantic structures  needed in the definition of both denotational and  operational semantics.

·      The translation semantics helps in evaluating the expressivity power of the new constructs by allowing an immediate comparison between a program that uses the new constructs and its translation in a Java program.

·      It allows an implementation of the execution support of the extended language completely retargetable on all the compilers developed for Java.

This approach in the design of HO extensions for Java is further discussed in \cite{bellia2008a} where the translation semantics of Java 1.4, extended with {\em m-parameters}, is defined and used to form the kernel \cite{bellia2008b} of a pre-processor for Java compilers.

The drawbacks of m\_parameters are the impossibility to

·      statically check type correctness and

Such drawbacks are both overcome in   Bellia2009a, Bellia2009b where  mc\_parameters are defined. Mc\_parameters have a type which specifies also the class hierarchy in which the passed method must be defined, allowing a static type checking and overloading static resolution. To maintain retargetability and portability of the implementation of the resulting language, the translation semantics of mc\_parameters is defined resorting to the use of anonymous and inner classes, involved in the Java methodology known as callback  \cite{horstmann2007}.

In 2006, the Java community started a debate about the opportunity to introduce function abstractions, improperly called closures, in the language. The proposals resulting from such a debate are contained in \cite{Bracha06,Cole06,Lee06} and more recently

\cite{Bracha08,Cole08,Reinhold09}. In such proposals Java is extended with different  closure forms  and other mechanisms with the aim to  allow a better use of closures and integration in the language (closure conversion, shared variables, loop abstraction). As a matter of fact, our paper \cite{bellia2005} about $\zeta_x$-calculus already  contained the  definition of a form of closures. In Bellia2009c we apply the translation semantics approach to the extension of Java with a form of closures which contains (takes in) many of the features of the above cited papers. As for higher order methods the approach guarantees the goals of portability and retargetability but is not well suited to the study  different and alternative definitions of closures and related mechanisms. For this reason we resorted to a minimal core calculus, more meaningful and suited to Java features, to extend it with closures. Such a calculus defined in Bellia2010a and Bellia2011 is  obtained extending Featherweight Java \cite{Igarashi01}.

The implementation of the language extended with m_parameters can be downloaded here

A dabate is currently under way on whether closure should be added to Java or not. Some links are:

1.

2.

3.

4.

A survey on Java Omega is in:

Marco Bellia and M. Eugenia Occhiuto, Java$\Omega$: Higher Order Programming in Java. in Java in Academia and in Research, IConcept Press, To appear
\begin {abstract}

The paper considers the problems and the solutions that are concerned with the extension of Java with Higher Order mechanisms.
We start from the motivations namely the code reusability and the code expressivity. Through the description of the Java$\Omega$

project we discuss the design of constructs for Higher Order methods, methods as parameters and for closures that can be integrated

in Java and whose implementation must preserve re-targetability and portability of the Java compilers and of the JVM. We give the

formal definition of such constructs, including the formalization of a translation semantics which can be converted into a source-to-

source translation and implemented as one-pass preprocessor. Examples of the use of the formalized constructs are included.
\end {abstract}

The paper contains the technical complements, of a paper that describes the extensions of Java 1.5 with Higher Order mechanisms.

It contains the complete tables of (i) The translation semantics of a form of closure for Java; (ii) The translation semantics of H.O.

methods with mc\_parameters as arguments; (iii) The translation semantics of Java extended with the above mechanisms put together;

(iv) Theorems and lemmas and proofs of all the the properties of the mechanisms and of the semantics discussed. The material

includes several technicalities and considerations that relate to the above mentioned results. In particular, (a.1) An unambiguous

grammar for Java 1.5; (a.2) A formalism used to define a translation semantics; (a.3) A semi-formal description of the callback

methodology in Java.

\end {abstract}

Recent papers are:

begin {abstract}
In the last years, the Java community has been arguing about adding closures to Java in order to improve expressivity. The debate has not yet terminated but all proposals seem to converge towards a notion of Simple Closures which contain only essential features. This paper addresses the problem of defining a rigorous semantics for Simple Closures. The technique adopted is well known and has already been used to prove interesting properties of the language. A minimal calculus is defined: Featherweight Java extended with Simple Closures. Syntax and semantics of such calculus are defined and type safety and backward compatibility are proved.
\end {abstract}

Marco Bellia and M. Eugenia Occhiuto, Properties of Java Simple Closures. Fundamenta Informatica , To appear
\begin {abstract}
In the last years, the Java community has been arguing about adding closures to Java in order to improve expressivity. The debate has not yet terminated but all proposals seem to converge towards a notion of Simple Closures which contain only the essential features of anonymous functions. This paper addresses the problem of defining a rigorous semantics for Simple Closures. The technique adopted is well known and has already been used to prove interesting properties of other extensions of Java. A minimal calculus is defined: Featherweight Java extended with Simple Closures. Syntax and semantics of such a calculus are defined and type safety, backward compatibility, and the abstraction property are proved. \end {abstract}

\begin {abstract}

\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.

\end {abstract}

by M.E.Occhiuto