Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/DARTS.6.2.9
URN: urn:nbn:de:0030-drops-132060
URL: https://drops.dagstuhl.de/opus/volltexte/2020/13206/
Huang, Xuejing ; Oliveira, Bruno C. d. S.
A Type-Directed Operational Semantics For a Calculus with a Merge Operator (Artifact)
| pdf-format: |
|
|
| artifact-format: |
|
Abstract
Our companion paper proposes a type-directed operational semantics (TDOS) for λ_i^{:}: a calculus with intersection types and a merge operator. The artifact contains the specification of λ_i^{:} and its TDOS, and related Coq code. λ_i^{:} is formalized using the locally nameless representation with cofinite quantification. The Coq definition and some infrastructure code are generated by Ott and LNgen. λ_i^{:} is inspired by two closely related calculi by Dunfield (2014) and Oliveira et al. (2016), and a simple variant of it is designed to demonstrate the possibility to match with them without any modification. To relate the two calculi with λ_i^{:}, a sound theorem on semantics and a completeness theorem on typing are proved for each variant. In addition, we extended the bidirectional typing of Oliveira et al.’s λ_i calculus, and designed an elaboration from it to λ_i^{:}, to show that many of λ_i^{:}’s explicit annotations can be inferred automatically.
BibTeX - Entry
@Article{huang_et_al:DARTS:2020:13206,
author = {Xuejing Huang and Bruno C. d. S. Oliveira},
title = {{A Type-Directed Operational Semantics For a Calculus with a Merge Operator (Artifact)}},
pages = {9:1--9:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2020},
volume = {6},
number = {2},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/13206},
URN = {urn:nbn:de:0030-drops-132060},
doi = {10.4230/DARTS.6.2.9},
annote = {Keywords: operational semantics, type systems, intersection types}
}
| Keywords: | operational semantics, type systems, intersection types | |
| Seminar: | DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020) | |
| Related Scholarly Article: | https://doi.org/10.4230/LIPIcs.ECOOP.2020.26 | |
| Issue date: | 2020 | |
| Date of publication: | 06.11.2020 |
