Conclusion
Liquid Types
Generalize Program Logics via Types
Expressive and Automatic
Liquid Types
Generalize Program Logics via Types
Expressive and Automatic
Take Home 1: Inference
Typecheck "templates"
Abstract Interpretation
Liquid Types
Generalize Program Logics via Types
Expressive and Automatic
Take Home 2: Uninterpreted Functions
Liquid Types
Generalize Program Logics via Types
Expressive and Automatic
Take Home 3: Laziness breaks partial correctness