Document Open Access Logo

A Type-Directed Operational Semantics For a Calculus with a Merge Operator (Artifact)

Authors Xuejing Huang , Bruno C. d. S. Oliveira

Thumbnail PDF

Artifact Description

  • Filesize: 482 kB
  • 4 pages

Document Identifiers

Author Details

Xuejing Huang
  • The University of Hong Kong, China
Bruno C. d. S. Oliveira
  • The University of Hong Kong, China


The authors wish to thank Bingchen Gong for testing the artifact, and the anonymous artifact reviewers for their comments and suggestions.

Cite AsGet BibTex

Xuejing Huang and Bruno C. d. S. Oliveira. A Type-Directed Operational Semantics For a Calculus with a Merge Operator (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 9:1-9:4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)



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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Software and its engineering → Object oriented languages
  • Software and its engineering → Polymorphism
  • operational semantics
  • type systems
  • intersection types


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering formal metatheory. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’08, page 3–15, New York, NY, USA, 2008. Association for Computing Machinery. URL:
  2. Brian Aydemir and Stephanie Weirich. Lngen: Tool support for locally nameless representations. Technical Report MS-CIS-10-24, Department of Computer and Information Science, University of Pennsylvania, June 2010. URL:
  3. Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. The Essence of Nested Composition (Artifact). Dagstuhl Artifacts Series, 4(3):5:1-5:2, 2018. URL:
  4. Arthur Charguéraud. The locally nameless representation. Journal of Automated Reasoning, 49(3):363-408, 2012. Google Scholar
  5. Arthur Charguéraud and François Pottier. Tlc: a non-constructive library for coq. URL:
  6. The Coq Development Team. The Coq Reference Manual, version 8.11.1, April 2020. Available electronically at URL:
  7. Dirk Merkel. Docker: lightweight linux containers for consistent development and deployment. Linux journal, 2014(239):2, 2014. Google Scholar
  8. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, et al. Ott: Effective tool support for the working semanticist. Journal of functional programming, 20(1):71-122, 2010. Google Scholar
  9. GHC Team. Ghc user’s guide documentation., 2020.
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail