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

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

Displayed time zone: Central Time (US & Canada) change

13:00 - 14:20
S-4Research Papers at SPLASH-I +12h
Chair(s): Karim Ali University of Alberta, Eli Tilevich Virginia Tech
13:00
20m
Talk
K-LLVM: A Relatively Complete Semantics of LLVM IR
Research Papers
Liyi Li University of Illinois at Urbana-Champaign, Elsa Gunter University of Illinois
Link to publication DOI Media Attached
13:20
20m
Talk
A Type-Directed Operational Semantics for a Calculus with a Merge Operator
Research Papers
Xuejing Huang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
Link to publication DOI Media Attached
13:40
20m
Talk
A big step from finite to infinite computationsSCICO Journal-First
Research Papers
Davide Ancona DIBRIS, University of Genova, Italy, Francesco Dagnino DIBRIS, University of Genova, Italy, Jurriaan Rot Radboud University Nijmegen, Elena Zucca University of Genova
Link to publication DOI Media Attached
14:00
20m
Talk
Static Type Analysis by Abstract Interpretation of Python Programs
Research Papers
Raphaël Monat Sorbonne Université — LIP6, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université
Link to publication DOI Media Attached File Attached

Mon 16 Nov

Displayed time zone: Central Time (US & Canada) change

01:00 - 02:20
S-4Research Papers at SPLASH-I
Chair(s): Elisa Gonzalez Boix Vrije Universiteit Brussel, Belgium, Atsushi Igarashi Kyoto University, Japan
01:00
20m
Talk
K-LLVM: A Relatively Complete Semantics of LLVM IR
Research Papers
Liyi Li University of Illinois at Urbana-Champaign, Elsa Gunter University of Illinois
Link to publication DOI Media Attached
01:20
20m
Talk
A Type-Directed Operational Semantics for a Calculus with a Merge Operator
Research Papers
Xuejing Huang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
Link to publication DOI Media Attached
01:40
20m
Talk
A big step from finite to infinite computationsSCICO Journal-First
Research Papers
Davide Ancona DIBRIS, University of Genova, Italy, Francesco Dagnino DIBRIS, University of Genova, Italy, Jurriaan Rot Radboud University Nijmegen, Elena Zucca University of Genova
Link to publication DOI Media Attached
02:00
20m
Talk
Static Type Analysis by Abstract Interpretation of Python Programs
Research Papers
Raphaël Monat Sorbonne Université — LIP6, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université
Link to publication DOI Media Attached File Attached