Sandro Stucki

The Essence of Dependent Object Types

Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. In A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (WadlerFest '16), in LNCS, volume 9600, pp. 249--272, Springer, 2016.


Focusing on path-dependent types, the paper develops foundations for Scala from first principles. Starting from a simple calculus D<: of dependent functions, it adds records, intersections and recursion to arrive at DOT, a calculus for dependent object types. The paper shows an encoding of System F with subtyping in D<: and demonstrates the expressiveness of DOT by modeling a range of Scala constructs in it.