ECOOP 2018
Sun 15 - Sat 21 July 2018 Amsterdam, Netherlands
co-located with ECOOP and ISSTA 2018
Fri 20 Jul 2018 16:50 - 17:15 at Zurich II - Formal Calculi Chair(s): Atsushi Igarashi

Calculi with disjoint intersection types support an introduction form for intersections called the merge operator, while retaining a coherent semantics. Disjoint intersections types have great potential to serve as a foundation for powerful, flexible and yet type-safe and easy to reason OO languages. This paper shows how to significantly increase the expressive power of disjoint intersection types by adding support for nested subtyping and composition, which enables simple forms of family polymorphism to be expressed in the calculus. The extension with nested sub- typing and composition is challenging, for two different reasons. Firstly, the subtyping relation that supports these features is non-trivial, especially when it comes to obtaining an algorithmic version. Secondly, the syntactic method used to prove coherence for previous calculi with disjoint intersection types is too inflexible, making it hard to extend those calculi with new features (such as nested subtyping). We show how to address the first problem by adapting and extending the Barendregt, Coppo and Dezani (BCD) subtyping rules for intersections with records and coercions. A sound and complete algorithmic system is obtained by using an approach inspired by Pierce’s work. To address the second problem we replace the syntactic method to prove coherence, by a semantic proof method based on logical relations. Our work has been fully formalized in Coq, and we have an implementation of our calculus.

Fri 20 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:15
Formal CalculiECOOP Research Papers at Zurich II
Chair(s): Atsushi Igarashi Kyoto University, Japan
16:00
25m
Research paper
FHJ: A Formal Model for Hierarchical Dispatching and Overriding
ECOOP Research Papers
Yanlin Wang University of Hong Kong, Haoyuan Zhang , Bruno C. d. S. Oliveira University of Hong Kong, China, Marco Servetto Victoria University of Wellington
DOI
16:25
25m
Research paper
Modeling infinite behaviour by corules
ECOOP Research Papers
Davide Ancona University of Genova, Francesco Dagnino DIBRIS, University of Genova, Italy, Elena Zucca University of Genova
DOI
16:50
25m
Research paper
The Essence of Nested Composition
ECOOP Research Papers
Xuan Bi The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, China, Tom Schrijvers KU Leuven
DOI