Programming with Refinement Types
An Introduction to LiquidHaskell
Ranjit Jhala, Eric Seidel, Niki Vazou
[PDF]
1.
LiquidHaskell: Verification of Haskell Code
1.1.
Software bugs are Everywhere
1.2.
Software bugs are Everywhere
1.3.
Goal: Make Bugs Difficult to Express
1.4.
Via compile-time sanity checks
1.5.
Fact Check: Haskell VS. Heartbleed
1.6.
How The Heartbleed Bug Works
1.7.
The Heartbleed Bug in Haskell
1.8.
True
is a bad argument
1.9.
But,
10
is a good argument
1.10.
More Bugs: Partial Functions
1.11.
More Bugs: Termination
1.12.
Goal: Extend Type System
1.13.
Plan
1.14.
Recap
1.15.
Evaluation
1.16.
Evaluation
1.17.
Conclusion
1.18.
Thank You!
2.
Simple Refinement Types
2.1.
Simple Refinement Types
2.2.
Example: Integers equal to
0
2.3.
Example: Natural Numbers
2.4.
Exercise: Positive Integers
2.5.
Refinement Type Checking
2.6.
A Term Can Have
Many
Types
2.7.
Predicate Subtyping
[NUPRL, PVS]
2.8.
Predicate Subtyping
[NUPRL, PVS]
2.9.
Example: Natural Numbers
2.10.
Example: Natural Numbers
2.11.
SMT
Automates Subtyping
2.12.
Contracts: Function Types
2.13.
Pre-Conditions
2.14.
Exercise: Pre-Conditions
2.15.
Precondition Checked at Call-Site
2.16.
Precondition Checked at Call-Site
2.17.
Recap
2.18.
Unfinished Business
3.
Data Types
3.1.
Example: Lists
3.2.
Specifying the Length of a List
3.3.
Specifying the Length of a List
3.4.
Using Measures
3.5.
Example:
Partial
Functions
3.6.
Naming Non-Empty Lists
3.7.
Totality Checking in Liquid Haskell
3.8.
Back to
average
3.9.
In bounds
take
3.10.
Catch the The Heartbleed Bug!
3.11.
Recap
4.
Termination Checking
4.1.
Why termination Checking?
4.2.
Example: Termination of
fib
4.3.
Proving Termination I
4.4.
User specified Termination Metrics
4.5.
Proving Termination
4.6.
Lexicographic Termination
4.7.
How about data types?
4.8.
User specified metrics on ADTs
4.9.
Mutual Recursive Functions
4.10.
Diverging Functions
4.11.
Proving Termination
4.12.
Recap
5.
Refinement Reflection
5.1.
Theorems about Haskell functions
5.2.
Theorems about Haskell functions
5.3.
Types As Theorems
5.4.
Make the theorems pretty!
5.5.
Make the theorems even prettier!
5.6.
Use more SMT knowledge
5.7.
Theorems about Haskell functions
5.8.
Refinement Reflection
5.9.
fib
is an uninterpreted function
5.10.
Reflection at Result Type
5.11.
Reflection at Result Type
5.12.
Structuring Proofs
5.13.
Reusing Proofs: The because operator
5.14.
Paper & Pencil style Proofs
5.15.
Another Paper & Pencil like Proof
5.16.
Generalizing monotonicity proof
5.17.
Theorem Application
5.18.
Recap
6.
Structural Induction
6.1.
The list data type
6.2.
Reflection of ADTs into the logic
6.3.
Reflection of Structural Inductive Functions
6.4.
Reflection of Non Recursive Functions
6.5.
Functor Laws: Identity
6.6.
Functor Laws: Distribution
6.7.
Functor Laws: Distribution, Solution
6.8.
Onto Monoid Laws
6.9.
Monoid Laws: Left Identity
6.10.
Monoid Laws: Left Identity, Solution
6.11.
Monoid Laws: Right Identity
6.12.
Monoid Laws: Right Identity, Solution
6.13.
Monoid Laws: Associativity
6.14.
Onto Monad Laws!
6.15.
Monoid Laws: Left Identity
6.16.
Monad Laws: Left Identity, Solution
6.17.
Monoid Laws: Right Identity
6.18.
Monoid Laws: Associativity
6.19.
Monoid Laws: Associativity
6.20.
Proving the Beta Equivalence Lemma
6.21.
Proving the bind function Lemma
6.22.
Summing up the proved laws
6.23.
Recap
7.
Case Study: MapReduce
7.1.
Implementation
7.2.
Use Case: Summing List
7.3.
Proving Code Equivalence
7.4.
Sum relevant Proofs
7.5.
Map Reduce Equivalence
7.6.
Append of Take and Drop
7.7.
List Definition
7.8.
List Manipulation
7.9.
Recap
7.10.
Thank You!
8.
Append is Associative
9.