An Introduction to Refinement Types
Ranjit Jhala
[PDF]
1.
Follow Along Here
1.1.
Whats this?
1.2.
The First
Bug
1.3.
Fast forward to Present Day
1.4.
Fast forward to Present Day
1.5.
Fast forward to Present Day
1.6.
Programming Languages Research
1.7.
Modern Languages
1.8.
Modern Languages
1.9.
Modern Languages
1.10.
Modern Languages?
1.11.
Well-typed programs can go very wrong!
1.12.
Well-typed programs can go very wrong!
1.13.
Well-typed programs can go very wrong!
1.14.
Division By Zero
1.15.
Division By Zero
1.16.
Missing Keys
1.17.
Missing Keys
1.18.
Missing Keys
1.19.
Segmentation Faults
1.20.
Segmentation Faults
1.21.
HeartBleeds
1.22.
HeartBleeds
1.23.
HeartBleeds
1.24.
Goal: Programmer
Extensible
Analysis
1.25.
Plan
1.26.
Evaluation
1.27.
Evaluation
1.28.
Evaluation
1.29.
Conclusion
1.30.
Current & Future Work
1.31.
Thank You!
2.
Simple Refinement Types
2.1.
Types
2.2.
Predicates
2.3.
Expressions
2.4.
Example: Integers equal to
0
2.5.
Example: Natural Numbers
2.6.
Exercise: Positive Integers
2.7.
Refinement Type Checking
2.8.
A Term Can Have
Many
Types
2.9.
A Term Can Have
Many
Types
2.10.
Predicate Subtyping
[NUPRL, PVS]
2.11.
Predicate Subtyping
[NUPRL, PVS]
2.12.
Example: Natural Numbers
2.13.
Example: Natural Numbers
2.14.
SMT
Automates Subtyping
2.15.
Contracts: Function Types
2.16.
Pre-Conditions
2.17.
Exercise: Pre-Conditions
2.18.
Precondition Checked at Call-Site
2.19.
Exercise: Check That Data
2.20.
Precondition Checked at Call-Site
2.21.
size
returns positive values
2.22.
Postconditions Checked at Return
2.23.
Verifying
avg
2.24.
Recap
2.25.
Unfinished Business
3.
Data Types
3.1.
Example: Lists
3.2.
Specifying the size of a List
3.3.
Specifying the size of a List
3.4.
Using Measures
3.5.
Exercise:
Partial
Functions
3.6.
Naming Non-Empty Lists
3.7.
head
and
tail
are Safe
3.8.
A Useful Partial Function: Fold / Reduce
3.9.
A Useful Partial Function: Fold / Reduce
3.10.
Exercise:
average
3.11.
Refining Data Types
3.12.
Example: Year is 12 Months
3.13.
Example: Year is 12 Months
3.14.
Exercise:
map
3.15.
Exercise:
init
3.16.
Exercise:
init'
3.17.
Recap
4.
Case Study: Insertion Sort
4.1.
Insertion Sort
4.2.
Goal: Verified Insertion Sort
4.3.
Property 1: Size
4.4.
Exercise:
insert
4.5.
Property 2: Elements
4.6.
Permutation
4.7.
SMT Solvers Reason About Sets
4.8.
Specifying A
List
s Elements
4.9.
Exercise: Verifying Permutation
4.10.
Property 3: Order
4.11.
Recall: Refined Data Types
4.12.
Refined Data: Ordered Pairs
4.13.
Exercise: Ordered Pairs
4.14.
Refined Data: CSV Tables
4.15.
Exercise: Valid CSV Tables
4.16.
Property 3: Ordered Lists
4.17.
Lists
4.18.
Ordered Lists
4.19.
Ordered Lists
4.20.
Exercise: Insertion Sort
4.21.
Multiple Measures
4.22.
Different Measures for
List
4.23.
Multiple Measures are Conjoined
4.24.
Recap
4.25.
Continue
5.
Termination Checking
5.1.
Why termination Checking?
5.2.
Example: Termination of
fib
5.3.
Proving Termination
5.4.
Example: Termination of
fib
5.5.
User Specified Termination Metrics
5.6.
User Specified Termination Metrics
5.7.
Proving Termination
5.8.
Lexicographic Termination
5.9.
How About Data Types?
5.10.
User specified metrics on ADTs
5.11.
Mutually Recursive Functions
5.12.
Diverging Functions
5.13.
Proving Termination
5.14.
Termination is Easy in Practice
5.15.
Termination is Easy in Practice
5.16.
Recap
5.17.
What properties can be expressed in the logic?
6.
Refinement Reflection
6.1.
Theorems about Haskell functions
6.2.
Theorems about Haskell functions
6.3.
Types As Theorems
6.4.
Make the theorems pretty!
6.5.
Make the theorems even prettier!
6.6.
Use more SMT knowledge
6.7.
Theorems about Haskell functions
6.8.
Refinement Reflection
6.9.
fib
is an uninterpreted function
6.10.
Reflect Function into Output Type
6.11.
Reflection at Result Type
6.12.
Structuring Proofs
6.13.
Reusing Proofs: The "because" operator
6.14.
Paper & Pencil style Proofs
6.15.
Another "Paper & Pencil" Proof
6.16.
Generalizing monotonicity proof
6.17.
Reusing Theorems by Application
6.18.
Recap
7.
Structural Induction
7.1.
The list data type
7.2.
Reflection of ADTs into the logic
7.3.
Reflection of Structural Inductive Functions
7.4.
Prove fancy lists properties
7.5.
Recap
7.6.
Appendix: Reflection of Non Recursive Functions
7.7.
Proving Map-Identity
7.8.
Automation: Proving Map-Identity
7.9.
Proving Map-Fusion
7.10.
Onto Monoid Laws
7.11.
Monoid Laws: Left Identity
7.12.
Monoid Laws: Right Identity
7.13.
Monoid Laws: Associativity
7.14.
Onto Monad Laws!
7.15.
Monoid Laws: Left Identity
7.16.
Monoid Laws: Right Identity
7.17.
Monoid Laws: Associativity
7.18.
Monoid Laws: Associativity
8.
Case Study: MapReduce
8.1.
MapReduce "Library"
8.2.
MapReduce "Client": Summing List
8.3.
Proving Code Equivalence
8.4.
Right Identity of
plus
8.5.
Distributivity of
sum
8.6.
Higher Order Map Reduce Theorem
8.7.
Right Identity of
plus
8.8.
Warmup: Associativity of Append
8.9.
Proof Automation: Associativity of Append
8.10.
Distributivity of
sum
8.11.
Recap
8.12.
Recap
8.13.
Appendix: Proof of
mRTheorem
8.14.
Append of Take and Drop
8.15.
List Definition
8.16.
List Manipulation