|
Proof methods for corecursive programs. Jeremy Gibbons and Graham Hutton. October 2000.
I was surprised to see that we haven't mentioned this paper before. It is quite useful for learning how to prove properties of functions producing infinite lists etc.
The paper presents four methods: fixpoint induction, the approximation lemma, coinduction, and fusion with unfold.
Posted to theory by Ehud Lamm on 8/10/03; 12:56:05 AM
|
Proof methods for corecursive programs
