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.
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.