Liquid Haskell

Verification with Refinement Types

Niki Vazou, IMDEA Software Institute

• I.Program Verification
• 1.Refinement Types
• 2.Data Types
• 3.Sortedness & Abstract Refinements
• 4.Termination
• II.Theorem Proving
• 5.Programs are Proofs
• 6.Structural Induction
• 7.Case Study: Map Reduce
• 8.Natural Deduction
• 9.Data Propositions