2026-07-25T09:20:12Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:14033 2024-03-06T11:05:12Z ddc:004 open_access

Type-Directed Operational Semantics for Gradual Typing (Artifact) Ye, Wenjia Oliveira, Bruno C. d. S. Huang, Xuejing Gradual Typing Operational Semantics Type Systems 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Wenjia Ye and Bruno C. d. S. Oliveira and Xuejing Huang 2021 Is Part Of DARTS, Volume 7, Issue 2, Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DARTS.7.2.9 urn:nbn:de:0030-drops-140337 https://drops.dagstuhl.de/entities/document/10.4230/DARTS.7.2.9 eng https://creativecommons.org/licenses/by/4.0/legalcode