Programming with Refinement Types An Introduction to LiquidHaskell Ranjit Jhala, Eric Seidel, Niki Vazou [PDF] 1.Introduction {#intro} 1.1. Well-Typed Programs Do Go Wrong {#gowrong} 1.2. Refinement Types 1.3. Audience 1.4. Getting Started 2.Logic & SMT 2.1. Syntax 2.2. Semantics {#semantics} 2.3. Verification Conditions 2.4. Examples: Propositions 2.5. Examples: Arithmetic 2.6. Examples: Uninterp