Java 与 Lambda：一个轻量级的故事
Java & Lambda: a Featherweight Story
AI总结：
该论文提出 FJ&$\lambda$ 核心演算，扩展 Featherweight Java 以支持接口、lambda 表达式和交集类型，形式化其在 Java 8 中的嫁接，并证明类型安全性质及给出类型推断算法。
摘要：
我们提出了 FJ&$\lambda$，一个新的核心演算，它扩展了 Featherweight Java（FJ），加入了接口，支持受限形式的多继承、$\lambda$ 表达式和交集类型。我们的主要目标是通过在形式化环境中研究其性质，来形式化 lambda 和交集类型如何嫁接到 Java 8 上。我们展示了交集类型在多种情况下发挥的重要作用，特别是在 $\lambda$ 表达式的类型转换和条件表达式的类型化中。我们还在 FJ&$\lambda$ 中体现了接口的默认方法，因为它们通过允许在 $\lambda$ 表达式上调用这些方法，增加了 $\lambda$ 表达式的动态性。在 Java 8 和我们的演算中，关键点在于 $\lambda$ 表达式可以根据上下文要求（目标类型）具有多种类型：实际上，当 $\lambda$ 表达式没有目标类型时，Java 代码无法编译。特别是，在操作语义中，我们必须通过装饰 $\lambda$ 表达式来记录目标类型，否则它们会在运行时表达式中丢失。我们证明了所得演算的主体归约性质和进展性质，并给出了一个类型推断算法，该算法在程序类型良好时返回给定程序的类型。FJ&$\lambda$ 的设计旨在使其成为 Java 8 的子集，同时保持 FJ 的优雅和简洁。实际上，FJ&$\lambda$ 程序与 Java 程序具有相同的类型和行为。
英文摘要：
We present FJ&$λ$, a new core calculus that extends Featherweight Java (FJ) with interfaces, supporting multiple inheritance in a restricted form, $λ$-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 $λ$-expression and in the typing of conditional expressions. We also embody interface \emph{default methods} in FJ&$λ$, since they increase the dynamism of $λ$-expressions, by allowing these methods to be called on $λ$-expressions. The crucial point in Java 8 and in our calculus is that $λ$-expressions can have various types according to the context requirements (target types): indeed, Java code does not compile when $λ$-expressions come without target types. In particular, in the operational semantics we must record target types by decorating $λ$-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&$λ$ has been driven by the aim of making it a subset of Java 8, while preserving the elegance and compactness of FJ. Indeed, FJ&$λ$ programs are typed and behave the same as Java programs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
