Type-Directed Operational Semantics for Gradual Typing (Artifact)

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

Thumbnail PDF

Artifact Description

  • Filesize: 0.67 MB
  • 6 pages

Document Identifiers

Author Details

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

Cite AsGet 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)



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
  • Gradual Typing
  • Operational Semantics
  • Type Systems


  • 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: 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. Arthur Charguéraud. The locally nameless representation. Journal of Automated Reasoning, 49(3):363-408, 2012. Google Scholar
  4. Arthur Charguéraud and François Pottier. Tlc: a non-constructive library for coq. URL: https://www.chargueraud.org/softs/tlc/.
  5. The Coq Development Team. The Coq Reference Manual, version 8.11.1, 2020. Available electronically at URL: https://coq.inria.fr/distrib/current/refman/.
  6. 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