License: Creative Commons Attribution 3.0 Germany license (CC BY 3.0 DE)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.3.2.5
URN: urn:nbn:de:0030-drops-72869
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7286/
Go back to Dagstuhl Artifacts Series

Wang, Fei ; Rompf, Tiark

Towards Strong Normalization for Dependent Object Types (DOT) (Artifact)

pdf-format:
DARTS-3-2-5.pdf (0.4 MB)

Abstract

This artifact provides the fully mechanized proof of strong normalization for D_{<:} , a variant of (Dependent Object Types) DOT (Rompf & Amin, 2016) that excludes recursive functions and recursive types. The intersection type and recursive self type are further integrated, moving towards DOT. The key proof idea follows the method of Girard (Girard, 1972) and Tait (Tait, 1967).

BibTeX - Entry

@Article{wang_et_al:DARTS:2017:7286,
  author =	{Fei Wang and Tiark Rompf},
  title =	{{Towards Strong Normalization for Dependent Object Types (DOT) (Artifact)}},
  pages =	{5:1--5:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2017},
  volume =	{3},
  number =	{2},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7286},
  URN =		{urn:nbn:de:0030-drops-72869},
  doi =		{10.4230/DARTS.3.2.5},
  annote =	{Keywords: Scala, DOT, strong normalization, logical relations, recursive types}
}

Keywords: Scala, DOT, strong normalization, logical relations, recursive types
Collection: DARTS, Volume 3, Issue 2
Related Scholarly Article: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2017.27
Issue Date: 2017
Date of publication: 20.06.2017

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