Theorem Proving for All

Equational Reasoning in Liquid Haskell

Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, and Graham Hutton

[PDF]

• 1.Introduction
• 2.Reasoning about Programs
• 2.1. Lightweight Reasoning
• 2.2. Induction on Lists
• 2.3. Proof Automation
• 3.Totality and Termination
• 3.1. Totality Checking
• 3.2. Termination Checking
• 3.3. Uncaught termination
• 4.Function Optimization
• 4.1. Example: Reversing a List
• 4.2. Example: Flattening a Tree
• 4.3. Appendix
• 5.Case Study: Correct Compilers
• 5.1. A simple stack machine
• 5.2. A note on totality
• 5.3. Compilation
• 5.4. Correctness
• 5.5. A faster compiler
• 5.6. Appendix
• 6.Related Work
• 6.1. Operator-based Equational Reasoning
• 6.2. Verification in Haskell
• 7.Conclusion