Programming with Refinement Types
An Introduction to LiquidHaskell
Ranjit Jhala, Eric Seidel, Niki Vazou
[PDF]
1.
Well-Typed Programs
Can
Go Wrong
1.1.
The Heartbleed Bug.
1.2.
The Heartbleed Bug in Haskell
1.3.
True
is a bad argument
1.4.
But,
10
is a good argument
1.5.
Partial Functions
1.6.
Functional Correctness
1.7.
Goal: Extend Type System
1.8.
Plan
1.9.
Evaluation
1.10.
Evaluation
1.11.
Evaluation
1.12.
Conclusion
1.13.
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 all the underlying logic
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.
Pencil & Paper like Proofs
5.15.
Higher Order Theorems
5.16.
Theorem Application
5.17.
Recap
6.
Case Study: MapReduce
6.1.
Implementation
6.2.
Use Case: Summing List
6.3.
Proving Code Equivalence
6.4.
Sum relevant Proofs
6.5.
Map Reduce Equivalence
6.6.
Append of Take and Drop
6.7.
List Definition
6.8.
List Manipulation
6.9.
Recap
6.10.
Thank You!