Strange Loop

Programming with Refinement Types

Haskell has many delightful features, perhaps the most beloved of which is its type system which allows developers to specify and verify a variety of program properties at compile time. However, many properties, typically those that depend on relationships between program values are impossible, or at the very least, cumbersome to encode within Haskell's type system.

Refinement types enable the specification and verification of value-dependent properties by extending Haskell's type system with logical predicates drawn from efficiently decidable logics.

In this workshop, we will start with a high level description of Refinement Types. Next, we will present an overview of LiquidHaskell, a refinement type checker for Haskell. In particular, we will describe the kinds of properties that can be checked, ranging from generic requirements like like totality (will 'head' crash?) and termination (will 'mergeSort' loop forever?), to application specific concerns like memory safety (will my code SEGFAULT?) and data structure correctness invariants (is this tree BALANCED?).

Joint work with: Niki Vazou, Eric Seidel, Patrick Rondon, Dimitris Vytiniotis and Simon Peyton-Jones.

Ranjit Jhala

Ranjit Jhala

UC San Diego

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.