Lectures on Liquid Haskell
Programming with Refinement Types
Niki Vazou
[PDF]
1.
Refinement Types
1.1.
Installation
1.2.
Basic Refinement Types
1.3.
Subtyping
1.4.
From Subtyping to Verification Conditions
1.5.
Verification Conditions
1.6.
Primitive Operations
1.7.
Function Types
1.8.
Branching and Recursion
1.9.
Refined Polymorphism
1.10.
Putting it all together: Safe Indexing
1.11.
Summary
1.12.
Further Reading
1.13.
Cheatsheet
2.
Data Types
2.1.
Measures
2.2.
Multiple Measures
2.3.
Recursive Functions
2.4.
Higher-Order Functions
2.5.
Folding (Indexed Lists)
2.6.
Data Invariants: Sparse Vectors
2.7.
Ordered Lists
2.8.
Summary
3.
Sortedness & Abstract Refinements
3.1.
Ordered Lists
3.2.
Abstraction over Sortedness
3.3.
Haskell's Lists
3.4.
Dependent Pairs
3.5.
Summary
4.
Termination
4.1.
Termination Requires Refinements!
4.2.
Termination Metrics
4.3.
Lexicographic Termination
4.4.
The GCD Example
4.5.
Data Types
4.6.
User Defined Data Types
4.7.
Mutual Recursion
4.8.
Summary
5.
Programs are Proofs
5.1.
Each Program Proves its type
5.2.
Propositions as Refinement Types
5.3.
Quantified Theorems
5.4.
Theorems about Haskell Functions
5.5.
Reusing Proofs, the "because" combinator
5.6.
Quantified Proofs
5.7.
Monotonicity of the Fibonacci Function
5.8.
Generalizing the Monotonicity Proof
5.9.
Proofs By Natural Induction
5.10.
Summary
6.
Structural Induction
6.1.
Structural Induction on Lists
6.2.
Map Fusion
6.3.
Monoid Laws for Lists
6.4.
Using Proved Lemma
6.5.
Summary
7.
Case Study: Map Reduce
7.1.
Map Reduce Explained
7.2.
Map Reduce "Library" Functions:
7.3.
Map Reduce "Client" Functions: Summing a List
7.4.
Proving Code Equivalence:
sum
and
psum
7.5.
Chunk Definition:
7.6.
Higher Order Theorem:
mRTheorem
7.7.
Lemmata for
mRTheorem
on plus
7.8.
Summary
7.9.
Appendix: List Manipulation Functions
8.
Natural Deduction
8.1.
Logical Properties
8.2.
Native Terms
8.3.
Conjunction
8.4.
Disjunction
8.5.
Implication
8.6.
Negation
8.7.
Forall
8.8.
Exists
8.9.
Example 1: existsAll
8.10.
Example 2: Distributing Qualifiers
8.11.
Example 3: List Properties
8.12.
Example 4: Natural Induction
8.13.
Summary
9.
Data Propositions
9.1.
Even Numbers
9.2.
Metatheory of Programming Languages
9.3.
Evaluation of Expressions
9.4.
Typing of Expressions
9.5.
Soundness = Progress + Preservation
9.6.
Summary
9.7.
Appendix: Missing Code
10.
Task 1: Program Verification
10.1.
1. Lists
10.2.
2. Insertion Sort
10.3.
3. Merge Sort
11.
Task 1: Program Verification
12.
Task 2: Proving Theorems
12.1.
1. Fusions
12.2.
2. Higher Order Properties
12.3.
3. Encoding of Logical Properties
13.
Task 2: Proving Theorems
13.1.
1. Fusions