Programming with Refinement Types
An Introduction to LiquidHaskell
Ranjit Jhala, Eric Seidel, Niki Vazou
[PDF]
1.
Liquid Haskell: Verification of Haskell Code
1.1.
Software bugs are Everywhere
1.2.
Software bugs are Everywhere
1.3.
How The Heartbleed Bug Works
1.4.
Goal: Make Bugs Difficult to Express
1.5.
Via compile-time sanity checks
1.6.
Fact Check: Haskell VS. Heartbleed
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: Program Equivalence
1.11.
More Bugs: Information Flow
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.
Example: Integers equal to
0
2.2.
Example: Natural Numbers
2.3.
Exercise: Positive Integers
2.4.
Type Checking
2.5.
SMTs to Automate Type Checking
2.6.
Refinement Reflection
2.7.
Theorems about Haskell functions
2.8.
Theorems about Haskell functions
2.9.
Types As Theorems
2.10.
Make the theorems pretty!
2.11.
Use more SMT knowledge
2.12.
Theorems about Haskell functions
2.13.
Refinement Reflection
2.14.
fib
is an uninterpreted function
2.15.
Reflection at Result Type
2.16.
Reflection at Result Type
2.17.
Structuring Proofs
2.18.
Reusing Proofs: The because operator
2.19.
Paper & Pencil style Proofs
2.20.
Another Paper & Pencil like Proof
2.21.
Generalizing monotonicity proof
2.22.
Theorem Application
2.23.
Application
3.
Resourses
3.1.
Plan
3.2.
Recap
3.3.
Evaluation
3.4.
Evaluation
3.5.
Conclusion
4.
Simple Refinement Types
4.1.
Simple Refinement Types
4.2.
Example: Integers equal to
0
4.3.
Example: Natural Numbers
4.4.
Exercise: Positive Integers
4.5.
Type Checking
4.6.
SMTs to Automate Type Checking
4.7.
Refinement Type Checking
4.8.
A Term Can Have
Many
Types
4.9.
Predicate Subtyping
[NUPRL, PVS]
4.10.
Predicate Subtyping
[NUPRL, PVS]
4.11.
Example: Natural Numbers
4.12.
Example: Natural Numbers
4.13.
SMT
Automates Implication Checking
4.14.
Contracts: Function Types
4.15.
Pre-Conditions
4.16.
Exercise: Pre-Conditions
4.17.
Precondition Checked at Call-Site
4.18.
Precondition Checked at Call-Site
4.19.
Recap
4.20.
Unfinished Business
5.
Data Types
5.1.
Example: Lists
5.2.
Specifying the Length of a List
5.3.
Specifying the Length of a List
5.4.
Using Measures
5.5.
Example:
Partial
Functions
5.6.
Naming Non-Empty Lists
5.7.
Totality Checking in Liquid Haskell
5.8.
Back to
average
5.9.
In bounds
take
5.10.
Catch the The Heartbleed Bug!
5.11.
Recap
6.
Termination Checking
6.1.
Why termination Checking?
6.2.
Example: Termination of
fib
6.3.
Proving Termination I
6.4.
User specified Termination Metrics
6.5.
Proving Termination
6.6.
Lexicographic Termination
6.7.
How about data types?
6.8.
User specified metrics on ADTs
6.9.
Mutual Recursive Functions
6.10.
Diverging Functions
6.11.
Proving Termination
6.12.
Recap
7.
Refinement Reflection
7.1.
Theorems about Haskell functions
7.2.
Theorems about Haskell functions
7.3.
Types As Theorems
7.4.
Make the theorems pretty!
7.5.
Make the theorems even prettier!
7.6.
Use more SMT knowledge
7.7.
Theorems about Haskell functions
7.8.
Refinement Reflection
7.9.
fib
is an uninterpreted function
7.10.
Reflection at Result Type
7.11.
Reflection at Result Type
7.12.
Structuring Proofs
7.13.
Reusing Proofs: The because operator
7.14.
Paper & Pencil style Proofs
7.15.
Another Paper & Pencil like Proof
7.16.
Generalizing monotonicity proof
7.17.
Theorem Application
7.18.
Recap
8.
Structural Induction
8.1.
The list data type
8.2.
Reflection of ADTs into the logic
8.3.
Reflection of Structural Inductive Functions
8.4.
Reflection of Non Recursive Functions
8.5.
Functor Laws: Identity
8.6.
Functor Laws: Identity
8.7.
Functor Laws: Distribution
8.8.
Functor Laws: Distribution, Solution
8.9.
Onto Monoid Laws
8.10.
Monoid Laws: Left Identity
8.11.
Monoid Laws: Left Identity, Solution
8.12.
Monoid Laws: Right Identity
8.13.
Monoid Laws: Right Identity, Solution
8.14.
Monoid Laws: Associativity
8.15.
Monoid Laws: Associativity, Solution
8.16.
Onto Monad Laws!
8.17.
Monoid Laws: Left Identity
8.18.
Monad Laws: Left Identity, Solution
8.19.
Monoid Laws: Right Identity
8.20.
Monoid Laws: Right Identity, Solution
8.21.
Monoid Laws: Associativity
8.22.
Monoid Laws: Associativity
8.23.
Monoid Laws: Associativity, Solution
8.24.
Proving the Beta Equivalence Lemma
8.25.
Summing up the proved laws
8.26.
Recap
9.
Case Study: MapReduce
9.1.
Implementation
9.2.
Use Case: Summing List
9.3.
Proving Code Equivalence
9.4.
Sum relevant Proofs
9.5.
Map Reduce Equivalence
9.6.
Append of Take and Drop
9.7.
List Definition
9.8.
List Manipulation
9.9.
Recap
9.10.
Thank You!
9.11.
Recap
10.
Information Flow Security
10.1.
LIFTY* (Liquid Information Flow TYpes)
10.2.
Example: Conference Managment System
10.3.
Policies as Refinement Types
10.4.
Policy Propagation: The Tagged Monad
10.5.
The Chair can see more...
10.6.
Program Repair
10.7.
More complex policies
10.8.
Recap
10.9.
Thank You!
11.
List Sorting
11.1.
Example: Lists
11.2.
Specifying the Length of a List
11.3.
Specifying the Length of a List
11.4.
Multiple Measures
11.5.
SMT Solvers Reason About Sets
11.6.
Specifying A
List
s Elements
11.7.
Multiple Measures
11.8.
Example : Inserting Elements
11.9.
Refining Data Types
11.10.
Example: Sorted Lists
11.11.
Ordered Lists
11.12.
Ordered Lists
11.13.
Exercise: Insertion Sort
11.14.
Refinements vs. Full Dependent Types
11.15.
Unfinished Business
11.16.
Recap
12.
Abstract Refinements
12.1.
Key Idea
12.2.
Ordered Lists
12.3.
Abstract Refinements on Data Structures
12.4.
Instantiation of Refinements
12.5.
Using Abstract Refinements
12.6.
Haskell's list
12.7.
Recap
13.
Bounded Refinement Types
13.1.
Verification of QuickSort (I)
13.2.
Ghost Variables
13.3.
Verification of
append
13.4.
Bounds on Abstract Refinements
13.5.
Bound Abstraction
13.6.
Bound Instantiations
13.7.
Recap
14.
Append is Associative
15.