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:20Talk K-LLVM: A Relatively Complete Semantics of LLVM IRResearch PapersLiyi LiUniversity of Illinois at Urbana-Champaign, Elsa GunterUniversity of Illinois Link to publication DOI Media Attached 13:20 - 13:40Talk A Type-Directed Operational Semantics for a Calculus with a Merge OperatorResearch PapersXuejing HuangThe University of Hong Kong, Bruno C. d. S. OliveiraUniversity of Hong Kong Link to publication DOI Media Attached 13:40 - 14:00Talk A big step from finite to infinite computationsSCICO Journal-FirstResearch PapersDavide 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:20Talk Static Type Analysis by Abstract Interpretation of Python ProgramsResearch PapersRaphaë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:20Talk K-LLVM: A Relatively Complete Semantics of LLVM IRResearch PapersLiyi LiUniversity of Illinois at Urbana-Champaign, Elsa GunterUniversity of Illinois Link to publication DOI Media Attached 01:20 - 01:40Talk A Type-Directed Operational Semantics for a Calculus with a Merge OperatorResearch PapersXuejing HuangThe University of Hong Kong, Bruno C. d. S. OliveiraUniversity of Hong Kong Link to publication DOI Media Attached 01:40 - 02:00Talk A big step from finite to infinite computationsSCICO Journal-FirstResearch PapersDavide 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:20Talk Static Type Analysis by Abstract Interpretation of Python ProgramsResearch PapersRaphaël MonatSorbonne Université — LIP6, Abdelraouf OuadjaoutSorbonne Université, Antoine MinéSorbonne Université Link to publication DOI Media Attached File Attached