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: https://drops.dagstuhl.de/opus/volltexte/2017/7286/
Wang, Fei ; Rompf, Tiark
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 = {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 | |
| 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: | 20.06.2017 |
