Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. SMT-Based Checking of Predicate-Qualified Types for Scala
 
conference paper

SMT-Based Checking of Predicate-Qualified Types for Scala

Schmid, Georg Stefan  
•
Kuncak, Viktor  
Biboudis, A
•
Jonnalagedda, M
Show more
2016
Scala'16: Proceedings Of The 2016 7Th Acm Sigplan Symposium On Scala
7th ACM SIGPLAN Symposium on 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.

  • Details
  • Metrics
Type
conference paper
DOI
10.1145/2998392.2998398
Web of Science ID

WOS:000390845300004

Author(s)
Schmid, Georg Stefan  
Kuncak, Viktor  
Editors
Biboudis, A
•
Jonnalagedda, M
•
Stucki, S
•
Ureche, V
Date Issued

2016

Publisher

Assoc Computing Machinery

Publisher place

New York

Published in
Scala'16: Proceedings Of The 2016 7Th Acm Sigplan Symposium On Scala
ISBN of the book

978-1-4503-4648-1

Total of pages

10

Start page

31

End page

40

Subjects

Scala

•

Refinement Types

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
LARA  
Event nameEvent placeEvent date
7th ACM SIGPLAN Symposium on Scala

Amsterdam, NETHERLANDS

OCT 30-31, 2016

Available on Infoscience
January 24, 2017
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/133873
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés