License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.7.2.9
URN: urn:nbn:de:0030-drops-140337
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14033/
Go back to Dagstuhl Artifacts Series

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

Type-Directed Operational Semantics for Gradual Typing (Artifact)

pdf-format:
DARTS-7-2-9.pdf (0.7 MB)

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.

BibTeX - Entry

@Article{ye_et_al:DARTS.7.2.9,
  author =	{Ye, Wenjia and Oliveira, Bruno C. d. S. and Huang, Xuejing},
  title =	{{Type-Directed Operational Semantics for Gradual Typing (Artifact)}},
  pages =	{9:1--9:6},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2021},
  volume =	{7},
  number =	{2},
  editor =	{Ye, Wenjia and Oliveira, Bruno C. d. S. and Huang, Xuejing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14033},
  URN =		{urn:nbn:de:0030-drops-140337},
  doi =		{10.4230/DARTS.7.2.9},
  annote =	{Keywords: Gradual Typing, Operational Semantics, Type Systems}
}

Keywords: Gradual Typing, Operational Semantics, Type Systems
Collection: DARTS, Volume 7, Issue 2, Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021)
Related Scholarly Article: https://doi.org/10.4230/LIPIcs.ECOOP.2021.12
Issue Date: 2021
Date of publication: 06.07.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI