2026-08-15T23:24:22Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7276 2024-03-06T10:39:46Z ddc:004 open_access

Towards Strong Normalization for Dependent Object Types (DOT) Wang, Fei Rompf, Tiark Scala DOT strong normalization logical relations recursive types The Dependent Object Types (DOT) family of calculi has been proposed as a new theoretic foundation for Scala and similar languages, unifying functional programming, object oriented programming and ML-style module systems. Following the recent type soundness proof for DOT, the present paper aims to establish stronger meta-theoretic properties. The main result is a fully mechanized proof of strong normalization for D_<:, a variant of DOT that excludes recursive functions and recursive types. We further discuss techniques and challenges for adding recursive types while maintaining strong normalization, and demonstrate that certain variants of recursive self types can be integrated successfully. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Fei Wang and Tiark Rompf 2017 Is Part Of LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2017.27 urn:nbn:de:0030-drops-72763 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.27 eng https://creativecommons.org/licenses/by/3.0/legalcode