[Pl-seminar] 10/10: Ranjit Jhala, Liquid Types For Haskell

[Vincent St-Amour]

NUPRL Seminar presents

Ranjit Jhala
University of California, San Diego

1:30 - 3:00
Friday, 10/10
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)


Liquid Types For Haskell

Abstract:
We present LiquidHaskell (http://goto.ucsd.edu/liquid), an automatic
verifier for Haskell. Liquid Haskell uses “Refinement types”, a
restricted form of dependent types where relationships between values
are encoded by decorating types with logical predicates drawn from an
efficiently SMT decidable theory (of arithmetic and uninterpreted
functions.) In this talk, we will describe the key ingredients of
LiquidHaskell.

First, we will present a rapid overview of liquid refinement types,
including SMT solver based (decidable) subtyping, and inference.
Decidability is achieved by eschewing the use of arbitrary terms inside
types, and the use of indices to encode rich properties of data.

Second, we will show how to recover some of the expressiveness lost by
restricting the logic, with two new techniques: measures which encode
structural properties of values and abstract refinements which enable
generalization (i.e. quantification) over refinements.

Third, we will discuss the curious interaction of laziness and
refinement typing. In a nutshell, the technique of refinement typing can
be viewed as a type-based generalization of Floyd-Hoare logics.
Surprisingly, we demonstrate that under non-strict evaluation, these
logics (and hence, classical refinement typing) are unsound, due to the
presence of potentially divergent sub-computations. Fortunately, we show
how soundness can be recovered with a termination analysis, itself,
circularly bootstrapped off refinement typing.

We have used LiquidHaskell to verify safety, functional correctness
and termination properties of real-world Haskell libraries totalling
more than 10,000 lines of code. Time permitting, we will present a
demonstration of the tool and a few short case studies illustrating its
use.