2026-07-25T05:43:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13206 2024-03-06T11:05:09Z ddc:004 open_access

A Type-Directed Operational Semantics For a Calculus with a Merge Operator (Artifact) Huang, Xuejing Oliveira, Bruno C. d. S. operational semantics type systems intersection types 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Xuejing Huang and Bruno C. d. S. Oliveira 2020 Is Part Of DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DARTS.6.2.9 urn:nbn:de:0030-drops-132060 https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.9 eng https://creativecommons.org/licenses/by/3.0/legalcode