文章基本信息

标题：Java & Lambda: a Featherweight Story
本地全文：下载
作者：Venneri, Betti ; Giannini, Paola ; Dezani-Ciancaglini, Mariangiola 等
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2018
卷号：14
期号：3
DOI：10.23638/LMCS-14(3:17)2018
语种：English
出版社：Technical University of Braunschweig
摘要：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 formalisehow lambdas and intersection types are grafted on Java 8, by studying theirproperties in a formal setting. We show how intersection types play asignificant role in several cases, in particular in the typecast of a$\lambda$-expression and in the typing of conditional expressions. We alsoembody interface \emph{default methods} in FJ&$\lambda$, since they increasethe dynamism of $\lambda$-expressions, by allowing these methods to be calledon $\lambda$-expressions. The crucial point in Java 8 and in our calculus is that $\lambda$-expressionscan have various types according to the context requirements (target types):indeed, Java code does not compile when $\lambda$-expressions come withouttarget types. In particular, in the operational semantics we must record targettypes by decorating $\lambda$-expressions, otherwise they would be lost in theruntime expressions. We prove the subject reduction property and progress for the resultingcalculus, and we give a type inference algorithm that returns the type of agiven program if it is well typed. The design of FJ&$\lambda$ has been drivenby the aim of making it a subset of Java 8, while preserving the elegance andcompactness of FJ. Indeed, FJ&$\lambda$ programs are typed and behave the sameas Java programs.
关键词：Computer Science - Logic in Computer Science;Computer Science - Programming Languages;03B70; 03B15; 68Q55