Liquid Haskell:
Verification of Haskell Code

Niki Vazou

(University of Maryland)




http://goto.ucsd.edu/~nvazou/presentations/shonan17/02-index.html










Resourses


github @ https://github.com/ucsd-progsys/liquidhaskell


book @ http://www.refinement-types.org


online demo @ http://goto.ucsd.edu/liquidhaskell


cabal install liquidhaskell










Plan


DONE

  1. Liquid Haskell 101
  2. Refinements Types: Types + Predicates + SMT
  3. Data Types: Measures for Structural Properties
  4. Termination Semantic Termination Checking
  5. Refinement Reflection Expressiveness

Coming up

  1. Proof Automation: Lists are Monads
  2. Case Study: Verification MapReduce

  3. Case Study: List Sorting
  4. Abstract Refinements
  5. Bounded Refinements