Refinement types for Haskell
Refinement types for Haskell,
Niki Vazou, Eric Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton Jones. ICFP 2014.
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
HALO: Haskell to Logic through Denotational Semantics
HALO: Haskell to Logic through Denotational Semantics,
Dimitrios Vytiniotis, Simon Peyton Jones, Koen Claessen, and Dan Rosen.
Submitted to POPL'13.
Even well-typed programs can go wrong, by encountering a pattern-match
failure, or simply returning the wrong answer. An
increasingly-popular response is to allow programmers to write
contracts that express semantic properties, such as
crash-freedom or some useful post-condition.
We study the static verification of such contracts.
Our main contribution is a novel translation to first-order logic
of both Haskell programs, and contracts written in Haskell,
all justified by denotational semantics. This translation enables us to prove
that functions satisfy their contracts using an off-the-shelf first-order logic
Static contract checking for Haskell
Static Contract checking for Haskell, Dana Xu, Simon Peyton Jones, and Koen Claessen. POPL'09.
Program errors are hard to detect and are costly both to programmers
who spend significant efforts in debugging, and for systems that are
guarded by runtime checks. Static verification techniques have been
applied to imperative and object-oriented languages, like Java and
C#, but few have been applied to a higher-order lazy functional
language, like Haskell. In this paper, we describe a sound and
automatic static verification tool for Haskell, that is based on
contracts and symbolic execution. Our approach is modular and gives precise blame
assignments at compile-time in the presence of higher-order functions
- A4 postscript
- Slides (PDF) of a talk given at the
Midlands Graduate School Christmas Lectures, 2007.
Errata. In Figure 2, in the right hand side of rule [E-match1], the ai and xi should both have vector arrows over them.
Extended static checking for Haskell
Extended static checking for Haskell, Dana Xu, Haskell Workshop 2006.
Abstract. Program errors are hard to detect and are costly both to
programmers who spend significant efforts in debugging, and to systems
that are guarded by runtime checks. Extended static checking can
reduce these costs by helping to detect bugs at compile-time, where
possible. Extended static checking has been applied to object-oriented
languages, like Java and C#, but it has not been applied to a lazy
functional language, like Haskell. In this paper, we describe an
extended static checking tool for Haskell, named ESC/Haskell, that is
based on symbolic computation and assisted by a few novel
strategies. One novelty is our use of Haskell as the specification
language itself for pre/post conditions. Any Haskell function
(including recursive and higher order functions) can be used in our
specification which allows sophisticated properties to be
expressed. To perform automatic verification, we rely on a novel
technique based on symbolic computation that is augmented by
counter-example guided unrolling. This technique can automate our
verification process and be efficiently implemented.