DARTS.7.2.9.pdf
- Filesize: 0.67 MB
- 6 pages
Document
Type-Directed Operational Semantics for Gradual Typing (Artifact)
Authors
Xuejing Huang 
-
Part of:
Issue:
Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021)
Volume: DARTS, Volume 7 (ECOOP 2021)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2021-07-06
Artifact Description
Document Identifiers
Author Details
Cite As Get BibTex
Wenjia Ye, Bruno C. d. S. Oliveira, and Xuejing Huang. Type-Directed Operational Semantics for Gradual Typing (Artifact). In Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021). Dagstuhl Artifacts Series (DARTS), Volume 7, Issue 2, pp. 9:1-9:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/DARTS.7.2.9
Artifact
DARTS-7-2-9-artifact-d9a38e1c93c960a4901f6aa9cb006062.tar
(Filesize: 2.92 GB)
MD5 Sum:
d9a38e1c93c960a4901f6aa9cb006062
(Get MD5 Sum)
Abstract
This artifact includes the Coq formalization associated with the paper Type-Directed Operational Semantics for Gradual Typing submitted in ECOOP 2021. The paper illustrates how to employ TDOS on gradually typed languages using two calculi. The first calculus, called λB, is inspired by the semantics of the blame calculus(λB^g) and is sound with λB^g. The second calculus, called λB^r, explores a different design space in the semantics of gradually typed languages. This document explains how to run the Coq formalization. Artifact can either be compiled in the pre-built docker image with all the dependencies installed or it could be built from the scratch. Sections 1-7 explain the basic information about the artifact. Section 7 explains how to get the docker image for the artifact. Section 8 explains the prerequisites and the steps to run coq files from scratch. Section 9 explains coq files briefly. Section 10 shows the correspondence of important lemmas, definitions and pictures discussed in the paper with their respective Coq formalization.
Subject Classification
ACM Subject Classification
- Software and its engineering → Object oriented languages
- Theory of computation → Type theory
- Software and its engineering → Polymorphism
Keywords
- Gradual Typing
- Operational Semantics
- Type Systems
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/.
-
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, 2020. Available electronically at URL: https://coq.inria.fr/distrib/current/refman/.
-
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.