Towards Semantic Type Soundness for Dependent Object Types and Scala with Logical Relations in Iris

Paolo Giarrusso

The metatheory of the Scala core type system (DOT), first established recently, is still hard to extend, like other systems combining subtyping and forms of dependent types. Soundness of important Scala features remains an open problem in theory and in practice. To obtain a more extensible metatheory, in ongoing work we prove in Coq soundness of DOT semantically. This is challenging, because in DOT variables can be in scope in their own type, objects can define mutually recursive and impredicative type members, and can contain evidence of subtyping relations that must be sound. We address these challenges by novel applications of step-indexing, as supported by the Iris logic. Our proof clarifies difficulties in past proofs; ongoing work on extensions, such as paths, appears encouraging.

Paolo Giarrusso is a postdoc at EPFL, Switzerland

---

Previous: Wiebe van Geest | Dependent Types for Invariants in Session Types
Next: Neil Yorke-Smith | The Constraint Programming Language MiniZinc