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

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.6.2.9.pdf
  • Filesize: 482 kB
  • 4 pages

Document Identifiers

Subject Classification

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

Metrics

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

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.

Cite As Get 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) https://doi.org/10.4230/DARTS.6.2.9

Author Details

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

Funding

This work has been sponsored by Hong Kong Research Grant Council project numbers 17210617 and 17209519.

Acknowledgements

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

Artifact

  MD5 Sum: 5e97dd3092724a9fd4898f5c9a529c84 (Get MD5 Sum)

Related Article

  • Xuejing Huang and Bruno C. d. S. Oliveira, "A Type-Directed Operational Semantics For a Calculus with a Merge Operator", in 34th European Conference on Object-Oriented Programming (ECOOP 2020), LIPIcs, Vol. 166, pp. 26:1 - 26:32, 2020. https://doi.org/10.4230/LIPIcs.ECOOP.2020.26

References

  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: https://doi.org/10.1145/1328438.1328443.
  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: https://repository.upenn.edu/cis_reports/933/.
  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: https://doi.org/10.4230/DARTS.4.3.5.
  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: https://www.chargueraud.org/softs/tlc/.
  6. The Coq Development Team. The Coq Reference Manual, version 8.11.1, April 2020. Available electronically at URL: https://coq.inria.fr/distrib/current/refman/.
  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. https://downloads.haskell.org/~ghc/latest/docs/users_guide.pdf, 2020.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact