Document Open Access Logo

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

Authors Fei Wang, Tiark Rompf

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.3.2.5.pdf
  • Filesize: 425 kB
  • 3 pages

Document Identifiers

Subject Classification

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

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

Cite As Get 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

Author Details

Fei Wang
Tiark Rompf

Artifact

  MD5 Sum: 3bc74da5f2828e59e9df5f8f7993baf6 (Get MD5 Sum)

Related Article

  • Fei Wang and Tiark Rompf, "Towards Strong Normalization for Dependent Object Types (DOT)", in 31st European Conference on Object-Oriented Programming (ECOOP 2017), LIPIcs, Vol. 74, pp. 27:1-27:25, 2017. https://doi.org/10.4230/LIPIcs.ECOOP.2017.27

References

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

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact