[Haskell-cafe] Two questions: lazy evaluation and Church-Rosser

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? === Gregory Woodhouse gregory.woodhouse@sbcglobal.net "Nothing is as powerful than an idea whose time has come." -- Victor Hugo