An Introduction to Refinement Types
Ranjit Jhala
[PDF]
1.
Two Tends in Program Verification
1.1.
Type-Theory-based theorem provers
1.2.
SMT-based verifiers
1.3.
Predictable & SMT-automated Verification
1.4.
Refinement Reflection
1.5.
Outline
1.6.
Evaluation
1.7.
Conclusion
1.8.
Thank you!
2.
Refinement Reflection
2.1.
Refinement Types
2.2.
Specification & Termination & Verification
2.3.
Propositions
2.4.
Universal & Existential Propositions
2.5.
Refinement Reflection
2.6.
Step 1: Definition
2.7.
Step 2: Reflection
2.8.
Step 3: Application
2.9.
Proof structure is not important ...
2.10.
Equational Proofs
2.11.
Equational Proofs in Practice
2.12.
“Because” Combinators
2.13.
Arithmetic and Ordering
2.14.
Induction
2.15.
Higher Order Reasoning
2.16.
Instantiation of Higher Order Theorems
2.17.
What about automation?
2.18.
Proof by Logical Evaluation (
PLE
)
2.19.
Summary:
2.20.
Haskell Sigs
3.
Case Study: MapReduce
3.1.
MapReduce "Library"
3.2.
MapReduce "Client": Summing List
3.3.
Proving Code Equivalence
3.4.
Right Identity of
plus
3.5.
Distributivity of
sum
3.6.
Higher Order Map Reduce Theorem
3.7.
Right Identity of
plus
3.8.
Warmup: Associativity of Append
3.9.
Proof Automation: Associativity of Append
3.10.
Distributivity of
sum
3.11.
Summary:
3.12.
Appendix: Proof of
mRTheorem
3.13.
Append of Take and Drop
3.14.
List Definition
3.15.
List Manipulation
4.
Encoding Natural Deduction
4.1.
Propositions as Types
4.2.
Natural Deduction as Type Derivation
4.3.
Exists over Forall in Natural Deduction
4.4.
Exists over Forall in Natural Deduction
4.5.
Exists over Forall in Haskell!
4.6.
Distributing Existentials
4.7.
Distributing Universals
4.8.
Properties of User Defined Datatypes
4.9.
Induction on Natural Numbers
4.10.
Summary:
4.11.
Haskell Sigs
4.12.
Code for Lists