ECOOP 2020
Sun 15 - Tue 17 November 2020 Online Conference
co-located with SPLASH 2020
Mon 16 Nov 2020 01:20 - 01:40 at SPLASH-I - S-4 Chair(s): Atsushi Igarashi, Elisa Gonzalez Boix
Sun 15 Nov 2020 13:20 - 13:40 at SPLASH-I - S-4 Chair(s): Karim Ali, Eli Tilevich

Calculi with disjoint intersection types and a merge operator provide general mechanisms that can subsume various other features. Such calculi can also encode highly dynamic forms of object composition, which capture common programming patterns in dynamically typed languages (such as JavaScript) in a fully statically typed manner. Unfortunately, unlike many other foundational calculi (such as System $F$, System $F_{<:}$ or Featherweight Java), recent calculi with the merge operator lack a (direct) operational semantics with standard and expected properties such as determinism and subject-reduction. Furthermore the metatheory for such calculi can only account for terminating programs, which is a significant restriction in practice.

This paper proposes a type-directed operational semantics (TDOS) for $\lambda_{i}^{:}$: a calculus with intersection types and a merge operator. The calculus is inspired by two closely related calculi by Dunfield (2014) and Oliveira et al. (2016). Although Dunfield proposes a direct small-step semantics for his calculus, his semantics lacks both determinism and subject-reduction. Using our TDOS we obtain a direct semantics for $\lambda_{i}^{:}$ that has both properties. To fully obtain determinism, the $\lambda_{i}^{:}$ calculus employs a disjointness restriction proposed in Oliveira et al.’s $\lambda_{i}$ calculus. As an added benefit the TDOS approach deals with recursion in a straightforward way, unlike $\lambda_{i}$ and subsequent calculi where recursion is problematic. To further relate $\lambda_{i}^{:}$ to the calculi by Dunfield and Oliveira et al. we show two results. Firstly, the semantics of $\lambda_{i}^{:}$ is sound with respect to Dunfield’s small-step semantics. Secondly, we show that the type system of $\lambda_{i}^{:}$ is complete with respect to the $\lambda_{i}$ type system. All results have been fully formalized in the Coq theorem prover.

Sun 15 Nov
Times are displayed in time zone: Central Time (US & Canada) change

13:00 - 14:20: S-4Research Papers at SPLASH-I +12h
Chair(s): Karim AliUniversity of Alberta, Eli TilevichVirginia Tech
13:00 - 13:20
Talk
Research Papers
Liyi LiUniversity of Illinois at Urbana-Champaign, Elsa GunterUniversity of Illinois
Link to publication DOI Media Attached
13:20 - 13:40
Talk
Research Papers
Xuejing HuangThe University of Hong Kong, Bruno C. d. S. OliveiraUniversity of Hong Kong
Link to publication DOI Media Attached
13:40 - 14:00
Talk
Research Papers
Davide AnconaDIBRIS, University of Genova, Italy, Francesco DagninoDIBRIS, University of Genova, Italy, Jurriaan RotRadboud University Nijmegen, Elena ZuccaUniversity of Genova
Link to publication DOI Media Attached
14:00 - 14:20
Talk
Research Papers
Raphaël MonatSorbonne Université — LIP6, Abdelraouf OuadjaoutSorbonne Université, Antoine MinéSorbonne Université
Link to publication DOI Media Attached File Attached

Mon 16 Nov
Times are displayed in time zone: Central Time (US & Canada) change

01:00 - 02:20: S-4Research Papers at SPLASH-I
Chair(s): Atsushi IgarashiKyoto University, Japan, Elisa Gonzalez BoixVrije Universiteit Brussel, Belgium
01:00 - 01:20
Talk
Research Papers
Liyi LiUniversity of Illinois at Urbana-Champaign, Elsa GunterUniversity of Illinois
Link to publication DOI Media Attached
01:20 - 01:40
Talk
Research Papers
Xuejing HuangThe University of Hong Kong, Bruno C. d. S. OliveiraUniversity of Hong Kong
Link to publication DOI Media Attached
01:40 - 02:00
Talk
Research Papers
Davide AnconaDIBRIS, University of Genova, Italy, Francesco DagninoDIBRIS, University of Genova, Italy, Jurriaan RotRadboud University Nijmegen, Elena ZuccaUniversity of Genova
Link to publication DOI Media Attached
02:00 - 02:20
Talk
Research Papers
Raphaël MonatSorbonne Université — LIP6, Abdelraouf OuadjaoutSorbonne Université, Antoine MinéSorbonne Université
Link to publication DOI Media Attached File Attached