Programming with Refinement Types

An Introduction to LiquidHaskell

Ranjit Jhala, Eric Seidel, Niki Vazou

[PDF]

• 1.Well-Typed Programs Can Go Wrong
• 1.1. Division By Zero
• 1.2. Missing Keys
• 1.3. Segmentation Faults
• 1.4. "HeartBleeds"
• 1.5. Goal: Extend Type System
• 1.6. Plan
• 1.7. Evaluation
• 1.8. Evaluation
• 1.9. Evaluation
• 1.10. Conclusion
• 1.11. Current & Future Work
• 1.12. Thank You!
• 2.Simple Refinement Types
• 2.1. Simple Refinement Types
• 2.2. Types
• 2.3. Predicates
• 2.4. Expressions
• 2.5. Example: Integers equal to 0
• 2.6. Example: Natural Numbers
• 2.7. Exercise: Positive Integers
• 2.8. Refinement Type Checking
• 2.9. A Term Can Have Many Types
• 2.10. A Term Can Have Many Types
• 2.11. Predicate Subtyping [NUPRL, PVS]
• 2.12. Predicate Subtyping [NUPRL, PVS]
• 2.13. Example: Natural Numbers
• 2.14. Example: Natural Numbers
• 2.15. SMT Automates Subtyping
• 2.16. Contracts: Function Types
• 2.17. Pre-Conditions
• 2.18. Exercise: Pre-Conditions
• 2.19. Precondition Checked at Call-Site
• 2.20. Exercise: Check That Data
• 2.21. Precondition Checked at Call-Site
• 2.22. size returns positive values
• 2.23. Postconditions Checked at Return
• 2.24. Verifying avg
• 2.25. Recap
• 2.26. 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. 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 Lists 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. Measures vs. Indexed Types
• 4.25. Refinements vs. Full Dependent Types
• 4.26. Continue
• 5.Case Study: Associative Maps & Evaluation
• 5.1. Associative Maps
• 5.2. Associative Maps & Evaluation
• 5.3. Associative Maps
• 5.4. A Simple Associative Map
• 5.5. Lets Banish Missing Key Exceptions!
• 5.6. Specifying the Set of keys
• 5.7. The Empty Map
• 5.8. Inserting a New Key-Value Binding
• 5.9. Exercise: Looking Up a Key's Value
• 5.10. Key Not Found Begone!
• 5.11. Well-Scoped Evaluators
• 5.12. Expressions
• 5.13. Values
• 5.14. Exercise: Operating on Values
• 5.15. Environments
• 5.16. Evaluate Using Environments
• 5.17. Free vs Bound Variables
• 5.18. Free Variables
• 5.19. Free Variables: Example
• 5.20. Well-scoped Expressions
• 5.21. Exercise: Well-Scoped eval
• 5.22. Exercise: Top-level Evaluation
• 5.23. Exercise: Checked Top-level Evaluation
• 5.24. Wrap Up: Associative Maps & Evaluation
• 5.25. Continue
• 6.Case Study: Low Level Memory
• 6.1. "HeartBleed" in Haskell
• 6.2. "HeartBleed" in Haskell (1/3)
• 6.3. "HeartBleed" in Haskell (2/3)
• 6.4. "HeartBleed" in Haskell (3/3)
• 6.5. Types Against Overflows
• 6.6. 1. Low-level Pointer API
• 6.7. API: Types
• 6.8. API: Operations (1/2)
• 6.9. API: Operations (2/2)
• 6.10. Example
• 6.11. 2. ByteString API
• 6.12. ByteString Type
• 6.13. Refined ByteString Type
• 6.14. Refined ByteString Type
• 6.15. Legal Bytestrings
• 6.16. Illegal Bytestrings
• 6.17. API create : Allocate and Fill a ByteString
• 6.18. API unsafeTake : Extract prefix of size n
• 6.19. API unpack : Convert ByteString into List of Char
• 6.20. 3. Application API
• 6.21. Revisit "HeartBleed"
• 6.22. "HeartBleed" no more
• 6.23. Recap: Types vs Overflows
• 6.24. Bonus Material
• 6.25. Nested ByteStrings