\( \require{color} \definecolor{kvcol}{RGB}{203,23,206} \definecolor{tycol}{RGB}{5,177,93} \definecolor{refcol}{RGB}{18,110,213} \newcommand{\quals}{\mathbb{Q}} \newcommand{\defeq}{\ \doteq\ } \newcommand{\subty}{\preceq} \newcommand{\True}{\mathit{True}} \newcommand{\Int}{\mathtt{Int}} \newcommand{\Nat}{\mathtt{Nat}} \newcommand{\Zero}{\mathtt{Zero}} \newcommand{\foo}[4]{{#1}^{#4} + {#2}^{#4} = {#3}^{#4}} \newcommand{\reft}[3]{\{\bindx{#1}{#2} \mid {#3}\}} \newcommand{\ereft}[3]{\bindx{#1}{\{#2 \mid #3\}}} \newcommand{\bindx}[2]{{#1}\!:\!{#2}} \newcommand{\reftx}[2]{\{{#1}\mid{#2}\}} \newcommand{\inferrule}[3][]{\frac{#2}{#3}\;{#1}} \newcommand{\kvar}[1]{\color{kvcol}{\mathbf{\kappa_{#1}}}} \newcommand{\llen}[1]{\mathtt{llen}(#1)} \)

Evaluation

Evaluation

LiquidHaskell Is For Real

18: {v : (IO ()) | v == Main.main}main = [Char] -> (IO ())putStrLn {v : [Char] | len v >= 0}"Easter Egg: to force Makefile"

Substantial Code Bases

10KLoc, 50+ Modules

Complex Properties

Memory Safety, Functional Correctness*, Termination

Inference is Crucial

Numbers

Library	LOC
`Data.List`	814
`Data.Set.Splay`	149
`Data.Vector.Algorithms`	1219
`HsColour`	1047
`Data.Map.Base`	1396
`Data.Text`	3125
`Data.Bytestring`	3501
Total	11251

Numbers

Library	LOC	Time
`Data.List`	814	26s
`Data.Set.Splay`	149	27s
`Data.Vector.Algorithms`	1219	89s
`HsColour`	1047	196s
`Data.Map.Base`	1396	174s
`Data.Text`	3125	499s
`Data.Bytestring`	3501	294s
Total	11251	1305s

Recap

Refinements: Types + Predicates
Subtyping: SMT Implication
Measures: Strengthened Constructors
Abstract: Refinements over functions and data
Evaluation
Conclusion