{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:15:30Z","timestamp":1775873730767,"version":"3.50.1"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2018,9,5]],"date-time":"2018-09-05T00:00:00Z","timestamp":1536105600000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2018,9,5]],"date-time":"2018-09-05T00:00:00Z","timestamp":1536105600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2018,9,5]],"date-time":"2018-09-05T00:00:00Z","timestamp":1536105600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["644298"],"award-info":[{"award-number":["644298"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["644235"],"award-info":[{"award-number":["644235"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"accepted":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>We present FJ&amp;amp;$\\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&amp;amp;$\\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&amp;amp;$\\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&amp;amp;$\\lambda$ programs are typed and behave the same as Java programs.<\/jats:p>","DOI":"10.23638\/lmcs-14(3:17)2018","type":"journal-article","created":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T13:36:12Z","timestamp":1743687372000},"source":"Crossref","is-referenced-by-count":2,"title":["Java &amp; Lambda: a Featherweight Story"],"prefix":"10.23638","volume":"Volume 14, Issue 3","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4481-8096","authenticated-orcid":false,"given":"Lorenzo","family":"Bettini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2533-0511","authenticated-orcid":false,"given":"Viviana","family":"Bono","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3341-0941","authenticated-orcid":false,"given":"Mariangiola","family":"Dezani-Ciancaglini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2239-9529","authenticated-orcid":false,"given":"Paola","family":"Giannini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6458-0305","authenticated-orcid":false,"given":"Betti","family":"Venneri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2018,9,5]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/arxiv.org\/pdf\/1801.05052v4","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/arxiv.org\/pdf\/1801.05052v4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T13:36:12Z","timestamp":1743687372000},"score":1,"resource":{"primary":{"URL":"http:\/\/lmcs.episciences.org\/4216"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,5]]},"references-count":0,"URL":"https:\/\/doi.org\/10.23638\/lmcs-14(3:17)2018","relation":{"has-preprint":[{"id-type":"arxiv","id":"1801.05052v3","asserted-by":"subject"},{"id-type":"arxiv","id":"1801.05052v2","asserted-by":"subject"},{"id-type":"arxiv","id":"1801.05052v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1801.05052","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1801.05052","asserted-by":"subject"}],"is-cited-by":[{"id-type":"doi","id":"10.1145\/3486610.3486894","asserted-by":"object"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,9,5]]},"article-number":"4216"}}