Scala 2016
Sun 30 - Mon 31 October 2016 Amsterdam, Netherlands
co-located with SPLASH 2016
Mon 31 Oct 2016 13:30 - 13:55 at Matterhorn 2 - Analysis, Testing & Verification Chair(s): Philipp Haller

We 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.

Mon 31 Oct

scala-2016
13:30 - 15:10: Scala - Analysis, Testing & Verification at Matterhorn 2
Chair(s): Philipp HallerKTH Royal Institute of Technology
scala-2016147791700000013:30 - 13:55
Talk
Georg Stefan SchmidEPFL, Switzerland, Viktor KuncakEPFL, Switzerland
DOI File Attached
scala-2016147791850000013:55 - 14:20
Talk
DOI File Attached
scala-2016147792000000014:20 - 14:45
Talk
Quentin StiévenartVrije Universiteit Brussel, Belgium, Jens NicolayVrije Universiteit Brussel, Belgium, Wolfgang De MeuterVrije Universiteit Brussel, Belgium, Coen De RooverVrije Universiteit Brussel, Belgium
DOI
scala-2016147792150000014:45 - 15:10
Talk
Kartik ChandraHenry M. Gunn High School, Rastislav BodikUniversity of Washington, USA
Media Attached