一句话：提出核心演算 FJ&λ，形式化 Java 8 的 lambda、交集类型与接口默认方法，并证明类型安全与推断。
论文关注 Java 8 中 lambda 表达式与交集类型缺乏紧凑形式化基础的问题，提出核心演算 FJ&λ。它在 Featherweight Java 上加入接口、受限多重继承、lambda 表达式、交集类型和接口默认方法，以刻画 target type 驱动下的 lambda 类型化与运行时行为。由于 Java 要求 lambda 必须有目标类型，演算在操作语义中通过标注保留目标类型，避免运行期丢失；交集类型在 lambda 类型转换和条件表达式类型化中起关键作用。作者证明 subject reduction 与 progress，并给出返回良类型程序类型的类型推断算法。设计上保持 FJ 的简洁性，使 FJ&λ 程序在类型和行为上与 Java 8 一致。
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.
@article{paperbot381,
title = {Java & Lambda: a Featherweight Story},
author = {Lorenzo Bettini and Viviana Bono and Mariangiola Dezani-Ciancaglini and Paola Giannini and Betti Venneri},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 3},
year = {2018},
doi = {10.23638/lmcs-14(3:17)2018}
}