Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Wang, Fei; Rompf, Tiark License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-72869
URL:

;

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

pdf-format:
artifact-format:


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 =	{1},
  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
Seminar: DARTS, Volume 3, Issue 2
Related Scholarly Article: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2017.27
Issue date: 2017
Date of publication: 2017


DROPS-Home | Fulltext Search | Imprint Published by LZI