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 $\lambda_{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 his calculus, his semantics lacks both determinism and subject-reduction. Using our TDOS we obtain a direct semantics for $\lambda_{i}^{:}$ that has both properties. To fully obtain determinism, the $\lambda_{i}^{:}$ calculus employs a disjointness restriction proposed in Oliveira et al.’s $\lambda_{i}$ calculus. As an added benefit the TDOS approach deals with recursion in a straightforward way, unlike $\lambda_{i}$ and subsequent calculi where recursion is problematic. To further relate $\lambda_{i}^{:}$ to the calculi by Dunfield and Oliveira et al. we show two results. Firstly, the semantics of $\lambda_{i}^{:}$ is sound with respect to Dunfield’s small-step semantics. Secondly, we show that the type system of $\lambda_{i}^{:}$ is complete with respect to the $\lambda_{i}$ type system. All results have been fully formalized in the Coq theorem prover.