LiquidHaskell takes as input haskell source code, annotated with specifications and checkes whether the code satisfies the specifications.

Specifications are expressed with liquid types, ie., a subset of dependent types for which inference and checking is decidable.

Try liquidHaskell

• Online: goto.ucsd.edu/liquidhaskell
• Github: ucsd-progsys/liquidhaskell
• Locally: `cabal install liquidhaskell`

Outline

1. Simple Refinements
   
2. Measures
   
3. Higher Order Refinements
   
4. Abstract Refinements
   
5. Inductive Refinements
   
6. Composing Refinements
   
7. Recursive Refinements
   
8. Indexed Refinements
9. Laziness
   
10. Benchmarks
    

Outline

Thank You!