Schmid, Georg StefanKuncak, Viktor2017-01-242017-01-242017-01-24201610.1145/2998392.2998398https://infoscience.epfl.ch/handle/20.500.14299/133873WOS:000390845300004We present qualified types for Scala, a form of refinement types adapted to the Scala language. Qualified types allow users to refine base types and classes using predicate expressions. We implemented a type checker for qualified types that is embedded in Scala's next-generation compiler Dotty and delegates constraint checking to an SMT solver. Our system supports many of Scala's functional as well as its object-oriented constructs. To propagate user-provided qualifier ascriptions we utilize both Scala's own type system and an incomplete, but effective qualifier inference algorithm. Our evaluation shows that for a series of examples exerting various of Scala's language features, the additional compile-time overhead is manageable. By combining these features we show that one can verify essential safety properties such as static bounds-checks while retaining several of Scala's advanced features.ScalaRefinement Typestext::conference output::conference proceedings::conference paper