skip to main content
Language:
Search Limited to: Search Limited to: Resource type Show Results with: Show Results with: Search type Index

Java Lambda: a Featherweight Story

Logical methods in computer science, 2018-09, Vol.14, Issue 3 [Peer Reviewed Journal]

EISSN: 1860-5974 ;DOI: 10.23638/LMCS-14(3:17)2018

Full text available

Citations Cited by
  • Title:
    Java Lambda: a Featherweight Story
  • Author: Lorenzo Bettini ; Viviana Bono ; Mariangiola Dezani-Ciancaglini ; Paola Giannini ; Betti Venneri
  • Subjects: 03b70, 03b15, 68q55 ; computer science - logic in computer science ; computer science - programming languages
  • Is Part Of: Logical methods in computer science, 2018-09, Vol.14, Issue 3
  • Description: 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.
  • Publisher: Logical Methods in Computer Science e.V
  • Language: English
  • Identifier: EISSN: 1860-5974
    DOI: 10.23638/LMCS-14(3:17)2018
  • Source: Alma/SFX Local Collection
    ROAD: Directory of Open Access Scholarly Resources
    DOAJ Directory of Open Access Journals

Searching Remote Databases, Please Wait