An Introduction to Refinement Types

Ranjit Jhala

[PDF]

• 1.Liquid Haskell: Verification of Haskell Code
• 1.1. Liquid Haskell: Verification of Haskell Code
• 1.2. Software bugs are Everywhere
• 1.3. Software bugs are Everywhere
• 1.4. How The Heartbleed Bug Works
• 1.5. How The Heartbleed Bug Works
• 1.6. How The Heartbleed Bug Works
• 1.7. Goal: Make Bugs Difficult to Express
• 1.8. Via compile-time sanity checks
• 1.9. Fact Check: Haskell VS. Heartbleed
• 1.10. The Heartbleed Bug in Haskell
• 1.11. True is a bad argument
• 1.12. But, 10 is a good argument
• 1.13. More Bugs: Functional Correctness
• 1.14. More Bugs: Program Equivalence
• 1.15. Goal: Extend Type System
• 1.16. Plan
• 1.17. Installation & Resources
• 1.18. Recap
• 1.19. Evaluation
• 1.20. Evaluation
• 1.21. Conclusion
• 1.22. Thank You!
• 2.Simple Refinement Types
• 2.1. Simple Refinement Types
• 2.2. Example: Integers equal to 0
• 2.3. Example: Natural Numbers
• 2.4. Exercise: Positive Integers
• 2.5. Type Checking
• 2.6. SMTs to Automate Type Checking
• 2.7. A Term Can Have Many Types
• 2.8. Predicate Subtyping [NUPRL, PVS]
• 2.9. Predicate Subtyping [NUPRL, PVS]
• 2.10. Example: Natural Numbers
• 2.11. Example: Natural Numbers
• 2.12. SMT Automates Implication Checking
• 2.13. Contracts: Function Types
• 2.14. Pre-Conditions
• 2.15. Exercise: Pre-Conditions
• 2.16. Precondition Checked at Call-Site
• 2.17. Precondition Checked at Call-Site
• 2.18. Recap
• 2.19. Unfinished Business
• 3.Data Types
• 3.1. Example: Lists
• 3.2. Specifying the Length of a List
• 3.3. Specifying the Length of a List
• 3.4. Example: Partial Functions
• 3.5. Naming Non-Empty Lists
• 3.6. Totality Checking in Liquid Haskell
• 3.7. Back to average
• 3.8. In bounds take
• 3.9. Catch the The Heartbleed Bug!
• 3.10. Recap
• 4.Case Study: Insertion Sort
• 4.1. Goal: Verified Insertion Sort
• 4.2. Property 1: Size
• 4.3. Exercise: insert
• 4.4. Property 2: Elements
• 4.5. Permutation
• 4.6. SMT Solvers Reason About Sets
• 4.7. Specifying A Lists Elements
• 4.8. Exercise: Verifying Permutation
• 4.9. Property 3: Order
• 4.10. Refined Data: Ordered Pairs
• 4.11. Exercise: Ordered Pairs
• 4.12. Refined Data: CSV Tables
• 4.13. Exercise: Valid CSV Tables
• 4.14. Property 3: Ordered Lists
• 4.15. Lists
• 4.16. Ordered Lists
• 4.17. Ordered Lists
• 4.18. Exercise: Insertion Sort
• 4.19. Multiple Measures
• 4.20. Different Measures for List
• 4.21. Multiple Measures are Conjoined
• 4.22. Recap
• 4.23. Continue