Java & Lambda: a Featherweight Story
Lorenzo Bettini, Viviana Bono, Mariangiola Dezani-Ciancaglini, Paola, Giannini, Betti Venneri

TL;DR
This paper introduces FJ&λ, a formal core calculus extending Featherweight Java with interfaces, lambdas, and intersection types, to model Java 8 features while ensuring type safety and providing a type inference algorithm.
Contribution
It formalizes Java 8's lambda expressions and intersection types within a lightweight calculus, including operational semantics and type inference, preserving Java's behavior.
Findings
Proves subject reduction and progress for FJ&λ
Provides a type inference algorithm for well-typed programs
Models Java 8 features like default methods and target types
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
