Here is material on understanding Lambda Calculus using PLT Redex:
In this zip directory you can find file lc-with-Redex.doc which is a short intro in Lambda Calculus and contains info on how to use the material that goes with the essay. I have included a very condenced note on a system even without lambda, which is called ‘combinatory logic’. My essay is adressed to Schemers and uses PLT Scheme, particularly PLT’s redex library. It has become somewhat more verbose than I had in mind originally. If you have any ideas how to condence and simplify further without loosing too much content and accuracy, I welcome your suggestions. Comments about inaccuracies and other faults are welcome too, of course. My essay does not contain any new views. It is a compilation of views taken from books that have inspired me. They are mentioned in the essay.
If the format of the above link does not suit you, give me a ping and I’ll try to send you the material in a format that suits you.
With thanks to Douglas R. Hofstadter, Daniel P Friedman, Matthias Felleisen, Roby Findler, Casey Klein and others, in all feasible orders.
— Jos
I did not read it yet; this is on my long list.
(via plt)