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. Goal: Algorithmic Software Verification
• 1.15. Goal: Algorithmic Software Verification
• 1.16. Outline
• 1.17. Outline
• 1.18. Outline
• 1.19. Outline
• 1.20. Outline
• 2.Simple Refinement Types
• 2.1. Types
• 2.2. Types
• 2.3. Predicates
• 2.4. Predicates
• 2.5. Predicates
• 2.6. Predicates
• 2.7. Predicates
• 2.8. Example: Singletons
• 2.9. Example: Natural Numbers
• 2.10. A Term Can Have Many Types
• 2.11. 1. Predicate Subtyping [NUPRL, PVS]
• 2.12. 1. Predicate Subtyping [NUPRL, PVS]
• 2.13. 1. Predicate Subtyping [NUPRL, PVS]
• 2.14. Example: Natural Numbers
• 2.15. Example: Natural Numbers
• 2.16. 2. Typing Applications (Function Calls)
• 2.17. 2. Typing Applications (Function Calls)
• 2.18. 2. Typing Applications (Function Calls)
• 2.19. 2. Typing Applications (Function Calls)
• 2.20. Recap: Refinement Types 101
• 2.21. Recap: Refinement Types 101
• 2.22. Recap: Refinement Types 101
• 3.Refinement Types by Example
• 3.1. Refinement Types by Example
• 3.2. Refinement Types by Example
• 3.3. Refinement Types by Example
• 3.4. Specifications: Pre-Conditions
• 3.5. Specifications: Post-Conditions
• 3.6. Refinement Types by Example
• 3.7. Verification: Vector Sum
• 3.8. Verification: Vector Sum
• 3.9. Verification: Vector Sum
• 3.10. Refinement Types by Example
• 3.11. Inference
• 3.12. Inference: Vector Sum
• 3.13. Inference: Vector Sum
• 3.14. Inference: Vector Sum
• 3.15. Inference: Vector Sum
• 3.16. Inference: Vector Sum
• 3.17. Inference: Vector Sum
• 3.18. Refinement Types by Example
• 3.19. Collections & Higher-Order Functions
• 3.20. Collections & Higher-Order Functions
• 3.21. Collections & Higher-Order Functions
• 3.22. Collections & Higher-Order Functions
• 3.23. Refinement Types by Example
• 3.24. Example: List average
• 3.25. Refinements for Datatypes
• 3.26. Measures Yield Refined Constructors
• 3.27. Example: map over Lists
• 3.28. Refinements for Datatypes
• 3.29. Refinements for Datatypes
• 3.30. Refinements for Datatypes
• 3.31. Refinement Types by Example
• 4.Invariants In Constructors
• 4.1. Invariants In Constructors
• 4.2. Invariants In Constructors
• 4.3. Invariants In Constructors
• 4.4. Abstracting Refinements
• 4.5. Abstracting Refinements
• 4.6. Abstracting Refinements
• 4.7. Using Abstract Refinements
• 4.8. Recap
• 4.9. Recap
• 4.10. Bounded Refinements
• 4.11. Bounded Refinements
• 4.12. Bounded Refinements
• 4.13. Bounded Refinements
• 5.LiquidHaskell
• 5.1. LiquidHaskell
• 5.2. LiquidHaskell
• 5.3. Evaluation
• 5.4. Recap: Refinement Types
• 5.5. Recap: Refinement Types
• 5.6. Recap: Refinement Types
• 5.7. Recap: Refinement Types
• 5.8. Many Friends, Many Directions
• 5.9. Thank You!