Tutorial: Type-Based Analysis of Higher-Order Programs
Niki Vazou
1
, Patrick M. Rondon
2
, Eric Seidel
1
, and Ranjit Jhala
1
1
UC San Diego
2
Google
Examples from LiquidHaskell
There are online on our blog
goto.ucsd.edu/~rjhala/liquid
Outline
Simple Refinements
Higher Order Refinements
Abstract Refinements
Inductive Refinements
Composing Refinements
Recursive Refinements
Indexed Refinements