  We present FJ&$\lambda$, a new core calculus that extends Featherweight Java
(FJ) with interfaces, supporting multiple inheritance in a restricted form,
$\lambda$-expressions, and intersection types. Our main goal is to formalise
how lambdas and intersection types are grafted on Java 8, by studying their
properties in a formal setting. We show how intersection types play a
significant role in several cases, in particular in the typecast of a
$\lambda$-expression and in the typing of conditional expressions. We also
embody interface \emph{default methods} in FJ&$\lambda$, since they increase
the dynamism of $\lambda$-expressions, by allowing these methods to be called
on $\lambda$-expressions.
  The crucial point in Java 8 and in our calculus is that $\lambda$-expressions
can have various types according to the context requirements (target types):
indeed, Java code does not compile when $\lambda$-expressions come without
target types. In particular, in the operational semantics we must record target
types by decorating $\lambda$-expressions, otherwise they would be lost in the
runtime expressions.
  We prove the subject reduction property and progress for the resulting
calculus, and we give a type inference algorithm that returns the type of a
given program if it is well typed. The design of FJ&$\lambda$ has been driven
by the aim of making it a subset of Java 8, while preserving the elegance and
compactness of FJ. Indeed, FJ&$\lambda$ programs are typed and behave the same
as Java programs.
