Undecidability of D

Abstract

Dependent Object Types (DOT) is a calculus with path dependent types, intersection types, and object selfreferences, which serves as the core calculus of Scala 3. Although the calculus has been proven sound, it remains open whether type checking in DOT is decidable. In this paper, we establish undecidability proofs of type checking and subtyping of D