SMT-Based Checking of Predicate-Qualified Types for Scala

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.


Editor(s):
Biboudis, A
Jonnalagedda, M
Stucki, S
Ureche, V
Published in:
Scala'16: Proceedings Of The 2016 7Th Acm Sigplan Symposium On Scala, 31-40
Presented at:
7th ACM SIGPLAN Symposium on Scala, Amsterdam, NETHERLANDS, OCT 30-31, 2016
Year:
2016
Publisher:
New York, Assoc Computing Machinery
ISBN:
978-1-4503-4648-1
Keywords:
Laboratories:




 Record created 2017-01-24, last modified 2018-03-17


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)