Programming with Refinement Types
An Introduction to LiquidHaskell
Ranjit Jhala, Eric Seidel, Niki Vazou
[PDF]
1.
Introduction
1.1.
Well-Typed Programs Do Go Wrong
1.2.
Refinement Types
1.3.
Audience
1.4.
Getting Started
1.5.
Sample Code
2.
Logic & SMT
2.1.
Syntax
2.2.
Semantics
2.3.
Verification Conditions
2.4.
Examples: Propositions
2.5.
Examples: Arithmetic
2.6.
Examples: Uninterpreted Function
2.7.
Recap
3.
Refinement Types
3.1.
Defining Types
3.2.
Errors
3.3.
Subtyping
3.4.
Writing Specifications
3.5.
Refining Function Types: Pre-conditions
3.6.
Refining Function Types: Post-conditions
3.7.
Testing Values: Booleans and Propositions
3.8.
Putting It All Together
3.9.
Recap
4.
Polymorphism
4.1.
Specification: Vector Bounds
4.2.
Verification: Vector Lookup
4.3.
Inference: Our First Recursive Function
4.4.
Higher-Order Functions: Bottling Recursion in a
loop
4.5.
Refinements and Polymorphism
4.6.
Recap
5.
Refined Datatypes
5.1.
Sparse Vectors Revisited
5.2.
Ordered Lists
5.3.
Ordered Trees
5.4.
Recap
6.
Boolean Measures
6.1.
Partial Functions
6.2.
Lifting Functions to Measures
6.3.
Recap
7.
Numeric Measures
7.1.
Wholemeal Programming
7.2.
Specifying List Dimensions
7.3.
Lists: Size Preserving API
7.4.
Lists: Size Reducing API
7.5.
Dimension Safe Vector API
7.6.
Dimension Safe Matrix API
7.7.
Recap
8.
Elemental Measures
8.1.
Talking about Sets
8.2.
Proving QuickCheck Style Properties
8.3.
Content-Aware List API
8.4.
Permutations
8.5.
Uniqueness
8.6.
Unique Zippers
8.7.
Recap
9.
Case Study: Okasaki's Lazy Queues
9.1.
Queues
9.2.
Sized Lists
9.3.
Queue Type
9.4.
Queue Operations
9.5.
Recap
10.
Case Study: Associative Maps
10.1.
Specifying Maps
10.2.
Using Maps: Well Scoped Expressions
10.3.
Implementing Maps: Binary Search Trees
10.4.
Recap
11.
Case Study: Pointers & Bytes
11.1.
HeartBleeds in Haskell
11.2.
Low-level Pointer API
11.3.
A Refined Pointer API
11.4.
Assumptions vs Guarantees
11.5.
ByteString API
11.6.
Application API
11.7.
Recap: Types Against Overflows
12.
Case Study: AVL Trees
12.1.
AVL Trees
12.2.
Specifying AVL Trees
12.3.
Smart Constructors
12.4.
Inserting Elements
12.5.
Rebalancing Trees
12.6.
Refactoring Rebalance
12.7.
Deleting Elements
12.8.
Functional Correctness