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

Authors Fei Wang, Tiark Rompf

Thumbnail PDF

Artifact Description

  • Filesize: 425 kB
  • 3 pages

Document Identifiers

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)



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).
  • Scala
  • DOT
  • strong normalization
  • logical relations
  • recursive types


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  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:
  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

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail