Thumbnail
Access Restriction
Subscribed

Author Seidel, Eric L. ♦ Vazou, Niki ♦ Vytiniotis, Dimitrios ♦ Jhala, Ranjit ♦ Peyton-Jones, Simon
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Computer programming, programs & data
Abstract SMT-based checking of refinement types for call-by-value languages is a well-studied subject. Unfortunately, the classical translation of refinement types to verification conditions is unsound under lazy evaluation. When checking an expression, such systems implicitly assume that all the free variables in the expression are bound to values. This property is trivially guaranteed by eager, but does not hold under lazy, evaluation. Thus, to be sound and precise, a refinement type system for Haskell and the corresponding verification conditions must take into account which subset of binders actually reduces to values. We present a stratified type system that labels binders as potentially diverging or not, and that (circularly) uses refinement types to verify the labeling. We have implemented our system in LIQUIDHASKELL and present an experimental evaluation of our approach on more than 10,000 lines of widely used Haskell libraries. We show that LIQUIDHASKELL is able to prove 96% of all recursive functions terminating, while requiring a modest 1.7 lines of termination-annotations per 100 lines of code.
Description Affiliation: University of California at San Diego, San Diego, CA, USA (Vazou, Niki; Seidel, Eric L.; Jhala, Ranjit) || Microsoft Research, Cambridge, United Kingdom (Vytiniotis, Dimitrios; Peyton-Jones, Simon)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1983-05-01
Publisher Place New York
Journal ACM SIGPLAN Notices (SIGP)
Volume Number 49
Issue Number 9
Page Count 14
Starting Page 269
Ending Page 282


Open content in new tab

   Open content in new tab
Source: ACM Digital Library