Proof methods for corecursive programs Export

@article{citeulike:311163, abstract = {Recursion is a well-known and powerful programming technique, with a wide variety of applications. The dual technique of corecursion is less well-known, but is increasingly proving to be just as useful. This article is a tutorial on the four main methods for proving properties of corecursive programs: fixpoint induction, the approximation (or take) lemma, coinduction, and fusion.}, author = {Gibbons, Jeremy and Hutton, Graham}, citeulike-article-id = {311163}, citeulike-linkout-0 = {http://citeseer.csail.mit.edu/context/1632144/375423}, citeulike-linkout-1 = {http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/corecursive.pdf}, journal = {Fundamenta Informaticae}, keywords = {algebraic-reasoning, corecursion, haskell}, number = {4}, pages = {353--366}, posted-at = {2005-09-03 06:35:22}, priority = {2}, title = {Proof methods for corecursive programs}, url = {http://citeseer.csail.mit.edu/context/1632144/375423}, volume = {66}, year = {2005} }

TY - JOUR ID - citeulike:311163 L3 - citeulike-article-id:311163 N2 - Recursion is a well-known and powerful programming technique, with a wide variety of applications. The dual technique of corecursion is less well-known, but is increasingly proving to be just as useful. This article is a tutorial on the four main methods for proving properties of corecursive programs: fixpoint induction, the approximation (or take) lemma, coinduction, and fusion. IS - 4 JF - Fundamenta Informaticae EP - 366 TI - Proof methods for corecursive programs VL - 66 SP - 353 KW - algebraic-reasoning KW - corecursion KW - haskell AU - Gibbons, Jeremy AU - Hutton, Graham PY - 2005///April/May UR - http://citeseer.csail.mit.edu/context/1632144/375423 ER -