Liquid Types

Abstract

Modern programming languages like Haskell or ML or Scala have type systems which allow developers to specify and verify a variety of program properties at compile time. However, many crucial correctness concerns, ranging from general requirements like memory safety ("Will my code SEGFAULT?"), totality ("Will a hash table lookup fail?") or termination ("Will my merge-sort loop forever?") to program specific concerns ("Will my AVL implementation properly balance trees?"), have traditionally remained well outside the scope of static typing.

In this talk, we describe a technique called Liquid Types which extends classical typing with ideas from program logics and abstract interpretation, to obtain a system capable of helping the programmer establish the above kinds of properties via automatic, compile time type checking.

We have implemented the method in a checker called LiquidHaskell, which we have used to verify safety, functional correctness and termination properties of several real-world Haskell libraries. Time permitting we will present a demonstration of the tool and a few short case studies illustrating its use.

Bio

Ranjit Jhala is a Professor of Computer Science and Engineering at the University of California, San Diego. He is interested in building algorithms and tools that help engineer reliable computer systems. His work draws from and contributes to the areas of Model Checking, Program Analysis, and Automated Deduction, and Type Systems. He has helped create several influential systems including the BLAST software model checker, RELAY race detector, MACE/MC distributed language and model checker, and is now working to sneak formal specification and verification into daily programming, under the disguise of types.