ECOOP 2020
Sun 15 - Tue 17 November 2020 Online Conference
co-located with SPLASH 2020
Mon 16 Nov 2020 11:40 - 12:00 at SPLASH-I - M-3 Chair(s): John Boyland, Peter Thiemann
Mon 16 Nov 2020 23:40 - 00:00 at SPLASH-I - M-3 Chair(s): Hidehiko Masuhara, Patrick Rein

Subtyping is a concept frequently encountered in many programming languages and calculi. Various forms of subtyping exist for different type system features, including intersection types, union types or bounded quantification. Normally these features are designed independently of each other, without exploiting obvious similarities (or dualities) between features. This paper proposes a novel methodology for designing subtyping relations that exploits duality between features. At the core of our methodology is a generalization of subtyping relations, which we call Duotyping. Duotyping is parameterized by the mode of the relation. One of these modes is theusual subtyping, while another mode is supertyping (the dual of subtyping). Using the mode it is possible to generalize the usual rules of subtyping to account not only for the intended behaviour of one particular language construct, but also of its dual. Duotyping brings multiple benefits, including: shorter specifications and implementations, dual features that come essentially for free, as well as new proof techniques for various properties of subtyping. To evaluate a design based on Duotyping against traditional designs, we formalized various calculi with common OOP features (including union types, intersection types and bounded quantification) in Coq in both styles. Our results show that the metatheory when using Duotyping does not come at a significant cost: the metatheory with Duotyping has similar complexity and size compared to the metatheory for traditional designs. However, we discover new features as duals to well-known features. Furthermore, we also show that Duotyping can significantly simplify transitivity proofs for many of the calculi studied by us.

Mon 16 Nov

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

11:00 - 12:20
M-3Research Papers at SPLASH-I +12h
Chair(s): John Boyland Univeristy of Wisconsin, Milwaukee, Peter Thiemann University of Freiburg, Germany
11:00
20m
Talk
Tackling the Awkward Squad for Reactive Programming: The Actor-Reactor Model
Research Papers
Sam Van den Vonder Vrije Universiteit Brussel, Thierry Renaux Vrije Universiteit Brussel, Bjarno Oeyen Vrije Universiteit Brussel, Joeri De Koster Vrije Universiteit Brussel, Belgium, Wolfgang De Meuter Vrije Universiteit Brussel
Link to publication DOI Pre-print Media Attached
11:20
20m
Talk
Lifting Sequential Effects to Control Operators
Research Papers
Colin Gordon Drexel University
Link to publication DOI Pre-print Media Attached
11:40
20m
Talk
The Duality of Subtyping
Research Papers
Bruno C. d. S. Oliveira University of Hong Kong, Shaobo Cui , Baber Rehman University of Hong Kong
Link to publication DOI Media Attached
12:00
20m
Talk
Data Consistency in Transactional Storage Systems: A Centralised Semantics
Research Papers
Shale Xiong ARM Research, Andrea Cerone Football Radar, Azalea Raad Imperial College London, Philippa Gardner Imperial College London
Link to publication DOI Media Attached
23:00 - 00:20
M-3Research Papers at SPLASH-I
Chair(s): Hidehiko Masuhara Tokyo Institute of Technology, Patrick Rein Hasso Plattner Institute
23:00
20m
Talk
Tackling the Awkward Squad for Reactive Programming: The Actor-Reactor Model
Research Papers
Sam Van den Vonder Vrije Universiteit Brussel, Thierry Renaux Vrije Universiteit Brussel, Bjarno Oeyen Vrije Universiteit Brussel, Joeri De Koster Vrije Universiteit Brussel, Belgium, Wolfgang De Meuter Vrije Universiteit Brussel
Link to publication DOI Pre-print Media Attached
23:20
20m
Talk
Lifting Sequential Effects to Control Operators
Research Papers
Colin Gordon Drexel University
Link to publication DOI Pre-print Media Attached
23:40
20m
Talk
The Duality of Subtyping
Research Papers
Bruno C. d. S. Oliveira University of Hong Kong, Shaobo Cui , Baber Rehman University of Hong Kong
Link to publication DOI Media Attached
00:00
20m
Talk
Data Consistency in Transactional Storage Systems: A Centralised Semantics
Research Papers
Shale Xiong ARM Research, Andrea Cerone Football Radar, Azalea Raad Imperial College London, Philippa Gardner Imperial College London
Link to publication DOI Media Attached