2026-07-24T17:52:21Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7286 2024-03-06T11:05:00Z ddc:004 open_access

Towards Strong Normalization for Dependent Object Types (DOT) (Artifact) Wang, Fei Rompf, Tiark Scala DOT strong normalization logical relations recursive types 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). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Fei Wang and Tiark Rompf 2017 Is Part Of DARTS, Volume 3, Issue 2, Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DARTS.3.2.5 urn:nbn:de:0030-drops-72869 https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.5 eng https://creativecommons.org/licenses/by/3.0/de/legalcode