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