File Download
  Links for fulltext
     (May Require Subscription)
Supplementary

Conference Paper: The Essence of Nested Composition

TitleThe Essence of Nested Composition
Authors
Keywordsnested composition
family polymorphism
intersection types
coherence
Issue Date2018
PublisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH. The Journal's web site is located at hhttp://www.dagstuhl.de/publikationen/lipics/
Citation
The 32nd European Conference on Object-Oriented Programming (ECOOP 2018), Amsterdam, The Netherlands, 16-21 July 2018. In Millstein, T (ed.). LIPICS - Leibniz International Proceedings in Informatics, 2018, v. 109, article no. 22, p. 22:1–22:33 How to Cite?
AbstractCalculi 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 subtyping 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.
Persistent Identifierhttp://hdl.handle.net/10722/301308
ISSN
2020 SCImago Journal Rankings: 0.540

 

DC FieldValueLanguage
dc.contributor.authorBi, X-
dc.contributor.authorDos Santos Oliveira, BC-
dc.contributor.authorSchrijvers, T-
dc.date.accessioned2021-07-27T08:09:12Z-
dc.date.available2021-07-27T08:09:12Z-
dc.date.issued2018-
dc.identifier.citationThe 32nd European Conference on Object-Oriented Programming (ECOOP 2018), Amsterdam, The Netherlands, 16-21 July 2018. In Millstein, T (ed.). LIPICS - Leibniz International Proceedings in Informatics, 2018, v. 109, article no. 22, p. 22:1–22:33-
dc.identifier.issn1868-8969-
dc.identifier.urihttp://hdl.handle.net/10722/301308-
dc.description.abstractCalculi 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 subtyping 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.-
dc.languageeng-
dc.publisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH. The Journal's web site is located at hhttp://www.dagstuhl.de/publikationen/lipics/-
dc.relation.ispartofLIPICS - Leibniz International Proceedings in Informatics-
dc.relation.ispartofThe 32nd European Conference on Object-Oriented Programming (ECOOP 2018)-
dc.rightsThis work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.-
dc.subjectnested composition-
dc.subjectfamily polymorphism-
dc.subjectintersection types-
dc.subjectcoherence-
dc.titleThe Essence of Nested Composition-
dc.typeConference_Paper-
dc.identifier.emailDos Santos Oliveira, BC: bruno@cs.hku.hk-
dc.identifier.authorityDos Santos Oliveira, BC=rp01786-
dc.description.naturepublished_or_final_version-
dc.identifier.doi10.4230/LIPIcs.ECOOP.2018.22-
dc.identifier.hkuros323725-
dc.identifier.volume109-
dc.identifier.spage22:1-
dc.identifier.epage22:33-
dc.publisher.placeGermany-

Export via OAI-PMH Interface in XML Formats


OR


Export to Other Non-XML Formats