Amin, NadaGrütter, Karl SamuelOdersky, MartinRompf, TiarkStucki, Sandro2016-01-222016-01-222016-01-22201610.1007/978-3-319-30936-1_14https://infoscience.epfl.ch/handle/20.500.14299/122617Focusing 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.CalculusDependent TypesScalatext::conference output::conference proceedings::conference paper