Niki Vazou
Eric L. Seidel
Simon Peyton-Jones
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.
- L. Augustsson. Cayenne - a language with dependent types. In ICFP, 1998. Google Scholar
Digital Library
- G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu. Type-based termination of recursive definitions.. Mathematical Structures in Computer Science, 2004. Google ScholarDigital Library
- J. F. Belo, M. Greenberg, A. Igarashi, and B. C. Pierce. Polymorphic contracts. In ESOP, 2011. Google ScholarDigital Library
- J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis. Refinement types for secure implementations. ACM TOPLAS, 2011. Google ScholarDigital Library
- Y. Bertot and P. Castéran. Coq'Art: The Calculus of Inductive Constructions. Springer Verlag, 2004.Google Scholar
- A. Bradley and Z. Manna. The Calculus of Computation: Decision Procedures With Application To Verification. Springer-Verlag, 2007. Google ScholarDigital Library
- E. Brady. Idris: general purpose programming with dependent types. In PLPV, 2013. Google ScholarDigital Library
- V. Capretta. General recursion via coinductive types. Logical Methods in Computer Science, 2005.Google ScholarCross Ref
- C. Casinghino, V. Sjöberg, and S. Weirich. Combining proofs and programs in a dependently typed language. In POPL, 2014. Google ScholarDigital Library
- R. L. Constable and S. F. Smith. Partial objects in constructive type theory. In LICS, 1987.Google Scholar
- L. de Moura and N. Bjãrner. Z3: An efficient SMT solver. 2008.Google Scholar
- D. Detlefs, G. Nelson, and J. B. Saxe. Simplify: a theorem prover for program checking. J. ACM, 2005. Google ScholarDigital Library
- J. Dunfield. Refined typechecking with Stardust. In PLPV, 2007. Google ScholarDigital Library
- C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In PLDI, 2002. Google ScholarDigital Library
- J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, and R. Thiemann. Automated termination proofs for Haskell by term rewriting. TPLS, 2011. Google ScholarDigital Library
- C. A. R. Hoare. Procedures and parameters: An axiomatic approach. In Symposium on Semantics of Algorithmic Languages. 1971.Google ScholarCross Ref
- J. Hughes, L. Pareto, and A. Sabry. Proving the correctness of reactive systems using sized types. In POPL, 1996. Google ScholarDigital Library
- L. Jia, J. A. Vaughan, K. Mazurak, J. Zhao, L. Zarko, J. Schorr, and S. Zdancewic. Aura: a programming language for authorization and audit. In ICFP, 2008. Google ScholarDigital Library
- N. D. Jones and N. Bohr. Termination analysis of the untyped lamba-calculus. In RTA, 2004.Google Scholar
- M. Kawaguchi, P. Rondon, and R. Jhala. Type-based data structure verification. In PLDI, 2009. Google ScholarDigital Library
- K.W. Knowles and C. Flanagan. Hybrid type checking. ACM TOPLAS, 2010. Google ScholarDigital Library
- G. Nelson. Techniques for program verification. Technical Report CSL81-10, Xerox Palo Alto Research Center, 1981.Google Scholar
- T. Nipkow. Hoare logics for recursive procedures and unbounded nondeterminism. In CSL, 2002. Google ScholarDigital Library
- U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers, 2007.Google Scholar
- S. R. Della Rocca and L. Paolini. The Parametric Lambda Calculus, A Metamodel for Computation. 2004. Google ScholarDigital Library
- P. Rondon, M. Kawaguchi, and R. Jhala. Liquid Types. In PLDI, 2008. Google ScholarDigital Library
- J. Rushby, S. Owre, and N. Shankar. Subtypes for specifications: Predicate subtyping in pvs. IEEE TSE, 1998. Google ScholarDigital Library
- D. Sereni and N. D. Jones. Termination analysis of higher-order functional programs. In APLAS, 2005. Google ScholarDigital Library
- W. Sonnex, S. Drossopoulou, and S. Eisenbach. Zeno: An automated prover for properties of recursive data structures. In TACAS, 2012. Google ScholarDigital Library
- M. Sulzmann, M. M. T. Chakravarty, S. L. Peyton-Jones, and K. Donnelly. System F with type equality coercions. In TLDI, 2007. Google ScholarDigital Library
- N. Swamy, J. Chen, C. Fournet, P-Y. Strub, K. Bhargavan, and J. Yang. Secure distributed programming with value-dependent types. In ICFP, 2011. Google ScholarDigital Library
- A. M. Turing. On computable numbers, with an application to the eintscheidungsproblem. In LMS, 1936.Google Scholar
- N. Vazou, P. Rondon, and R. Jhala. Abstract refinement types. In ESOP, 2013. Google ScholarDigital Library
- N. Vazou, E. L. Seidel, and R. Jhala. Liquidhaskell: Experience with refinement types in the real world. In Haskell Symposium, 2014.Google ScholarDigital Library
- D. Vytiniotis, S. L. Peyton-Jones, K. Claessen, and D. Rosén. Halo: haskell to logic through denotational semantics. In POPL, 2013. Google ScholarDigital Library
- H. Xi. Dependent types for program termination verification. In LICS, 2001. Google ScholarDigital Library
- H. Xi and F. Pfenning. Eliminating array bound checking through dependent types. In PLDI, 1998. Google ScholarDigital Library
- D. N. Xu, S. L. Peyton-Jones, and K. Claessen. Static contract checking for haskell. In POPL, 2009. Google ScholarDigital Library
Index Terms
- Refinement types for Haskell
Recommendations
Refinement types for Haskell
ICFP '14SMT-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 ...
Refinement types for Haskell
PLPV '14: Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages meets Program VerificationWe present LiquidHaskell (http://goto.ucsd.edu/liquid), an automatic verifier for Haskell. LiquidHaskell uses Refinement types, a restricted form of dependent types where relationships between values are encoded by decorating types with logical ...
Gradual refinement types
POPL '17Refinement types are an effective language-based verification technique. However, as any expressive typing discipline, its strength is its weakness, imposing sometimes undesired rigidity. Guided by abstract interpretation, we extend the gradual typing ...
Comments