DARTS.6.2.9.pdf
- Filesize: 482 kB
- 4 pages
Document
A Type-Directed Operational Semantics For a Calculus with a Merge Operator (Artifact)
Authors
Xuejing Huang 
,
-
Part of:
Issue:
Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)
Volume: DARTS, Volume 6 (ECOOP 2020)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-11-06
Artifact Description
Document Identifiers
Author Details
Acknowledgements
The authors wish to thank Bingchen Gong for testing the artifact, and the anonymous artifact reviewers for their comments and suggestions.
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
Artifact
DARTS-6-2-9-artifact-5e97dd3092724a9fd4898f5c9a529c84.zip
(Filesize: 0.98 GB)
MD5 Sum:
5e97dd3092724a9fd4898f5c9a529c84
(Get MD5 Sum)
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.
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)
0PDF Downloads
References
- 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.
- 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/.
- 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.
-
Arthur Charguéraud. The locally nameless representation. Journal of Automated Reasoning, 49(3):363-408, 2012.
- Arthur Charguéraud and François Pottier. Tlc: a non-constructive library for coq. URL: https://www.chargueraud.org/softs/tlc/.
- 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/.
-
Dirk Merkel. Docker: lightweight linux containers for consistent development and deployment. Linux journal, 2014(239):2, 2014.
-
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.
- GHC Team. Ghc user’s guide documentation. https://downloads.haskell.org/~ghc/latest/docs/users_guide.pdf, 2020.