Gregory, Church-Rosser is proved in any good text on lambda calculus, such as Barendregt [1]. Some rather detailed notes on that book are at [2]. Lazy evaluation is often formalized as "call-by-need." Try [3]. Ezra [1] Barendregt. The Lambda Calculus http://www.amazon.com/exec/obidos/ASIN/0444875085 [2] http://www.andrew.cmu.edu/user/cebrown/notes/barendregt.html [3] Maraist, Odersky, and Wadler, "A call-by-need lambda-calculus." Journal of Functional Programming 8(3):275-317 (May 1998). http://homepages.inf.ed.ac.uk/wadler/topics/call-by-need.html On Nov 15, 2005, at 5:30 AM, Gregory Woodhouse wrote:

This is surely a dumb question, but where can I find a proof of the Church-Rosser theorem?

Now, a totally(?) separate question: I've been trying to do some background reading on lambda calculus, and have found discussions of strict evaluation strategies (call-by-value and call-by-name) but have yet to find an appropriate framework for modeling lazy evaluation (much less infinite lists and comprehensions). Can anyone point me in the right direction?