File Download
Links for fulltext
(May Require Subscription)
- Publisher Website: 10.4230/LIPIcs.ECOOP.2020.26
- Scopus: eid_2-s2.0-85115243747
- Find via
Supplementary
-
Citations:
- Scopus: 0
- Appears in Collections:
Conference Paper: A Type-Directed Operational Semantics For a Calculus with a Merge Operator
Title | A Type-Directed Operational Semantics For a Calculus with a Merge Operator |
---|---|
Authors | |
Keywords | operational semantics type systems intersection types |
Issue Date | 2020 |
Publisher | Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH. The Journal's web site is located at hhttp://www.dagstuhl.de/publikationen/lipics/ |
Citation | The 34th European Conference on Object-Oriented Programming (ECOOP 2020), Virtual Conference, Berlin, Germany, 15-17 November 2020. In Hirschfeld, R & Pape, T (Eds.). LIPICS - Leibniz International Proceedings in Informatics, 2020, v. 166, article no. 26, p. 26:1-26:32 How to Cite? |
Abstract | 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 λ_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 her calculus, her semantics lacks both determinism and subject-reduction. Using our TDOS we obtain a direct semantics for λ_i^{:} that has both properties. To fully obtain determinism, the λ_i^{:} calculus employs a disjointness restriction proposed in Oliveira et al.’s λ_i calculus. As an added benefit the TDOS approach deals with recursion in a straightforward way, unlike λ_i and subsequent calculi where recursion is problematic. To further relate λ_i^{:} to the calculi by Dunfield and Oliveira et al. we show two results. Firstly, the semantics of λ_i^{:} is sound with respect to Dunfield’s small-step semantics. Secondly, we show that the type system of λ_i^{:} is complete with respect to the λ_i type system. All results have been fully formalized in the Coq theorem prover. |
Persistent Identifier | http://hdl.handle.net/10722/301428 |
ISSN | 2020 SCImago Journal Rankings: 0.540 |
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Huang, X | - |
dc.contributor.author | Dos Santos Oliveira, BC | - |
dc.date.accessioned | 2021-07-27T08:10:55Z | - |
dc.date.available | 2021-07-27T08:10:55Z | - |
dc.date.issued | 2020 | - |
dc.identifier.citation | The 34th European Conference on Object-Oriented Programming (ECOOP 2020), Virtual Conference, Berlin, Germany, 15-17 November 2020. In Hirschfeld, R & Pape, T (Eds.). LIPICS - Leibniz International Proceedings in Informatics, 2020, v. 166, article no. 26, p. 26:1-26:32 | - |
dc.identifier.issn | 1868-8969 | - |
dc.identifier.uri | http://hdl.handle.net/10722/301428 | - |
dc.description.abstract | 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 λ_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 her calculus, her semantics lacks both determinism and subject-reduction. Using our TDOS we obtain a direct semantics for λ_i^{:} that has both properties. To fully obtain determinism, the λ_i^{:} calculus employs a disjointness restriction proposed in Oliveira et al.’s λ_i calculus. As an added benefit the TDOS approach deals with recursion in a straightforward way, unlike λ_i and subsequent calculi where recursion is problematic. To further relate λ_i^{:} to the calculi by Dunfield and Oliveira et al. we show two results. Firstly, the semantics of λ_i^{:} is sound with respect to Dunfield’s small-step semantics. Secondly, we show that the type system of λ_i^{:} is complete with respect to the λ_i type system. All results have been fully formalized in the Coq theorem prover. | - |
dc.language | eng | - |
dc.publisher | Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH. The Journal's web site is located at hhttp://www.dagstuhl.de/publikationen/lipics/ | - |
dc.relation.ispartof | LIPICS - Leibniz International Proceedings in Informatics | - |
dc.relation.ispartof | The 34th European Conference on Object-Oriented Programming (ECOOP 2020 | - |
dc.rights | This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License. | - |
dc.subject | operational semantics | - |
dc.subject | type systems | - |
dc.subject | intersection types | - |
dc.title | A Type-Directed Operational Semantics For a Calculus with a Merge Operator | - |
dc.type | Conference_Paper | - |
dc.identifier.email | Dos Santos Oliveira, BC: bruno@cs.hku.hk | - |
dc.identifier.authority | Dos Santos Oliveira, BC=rp01786 | - |
dc.description.nature | published_or_final_version | - |
dc.identifier.doi | 10.4230/LIPIcs.ECOOP.2020.26 | - |
dc.identifier.scopus | eid_2-s2.0-85115243747 | - |
dc.identifier.hkuros | 323740 | - |
dc.identifier.volume | 166 | - |
dc.identifier.spage | 26:1 | - |
dc.identifier.epage | 26:32 | - |
dc.publisher.place | Germany | - |