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

Wang, Fei; Rompf, Tiark

doi:10.4230/DARTS.3.2.5

Artifact Description

DARTS.3.2.5.pdf

Filesize: 425 kB
3 pages

Document Identifiers

DOI: 10.4230/DARTS.3.2.5
URN: urn:nbn:de:0030-drops-72869

Author Details

Fei Wang

Tiark Rompf

Cite AsGet BibTex

Fei Wang and Tiark Rompf. Towards Strong Normalization for Dependent Object Types (DOT) (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 5:1-5:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/DARTS.3.2.5

Artifact

DARTS-3-2-5-artifact-3bc74da5f2828e59e9df5f8f7993baf6.zip (Filesize: 37 kB)

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).

Keywords

Scala
DOT
strong normalization
logical relations
recursive types

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

References

Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII, 1972.
The Coq development team. The Coq proof assistant reference manual, 2012. Version 8.4. URL: http://coq.inria.fr.
Tiark Rompf and Nada Amin. Type soundness for dependent object types (DOT). In OOPSLA, pages 624-641. ACM, 2016.
William W. Tait. Intensional interpretations of functionals of finite type I. J. Symb. Log., 32(2):198-212, 1967.