# Test cases for λ-Calculus

For testing automated theorem provers we have Seventy-Five Problems for Testing Automatic Theorem Provers by Pelletier.

Are there any such standard/well regarded tests for a λ-calculus that verify the evaluation?

EDIT

The best λ-Calculus evaluator I have found so far is:

Lambda calculus reduction workbench with info here.

I like this one because
1. It is a working example that seems to corretly pass every example I can find.
2. Has a trace option for the output.
3. Can do multiple reduction strategies
* normal order
* call-by-name
* call-by-value
* applicative order
* hybrid normal order
* hybrid applicative order
4. Has a list of pre defined abbreavtions such as
* S, K, I
* 0 - 5
* pair
* pred
* succ
What would you like to test? Whether the evaluation works correctly? These days cool people prove it works using a theorem prover (which uses $\lambda$-calculus underneath...) –  Andrej Bauer Jan 17 '13 at 22:15
Coq would be an obvious one. Just implement Church numerals and compute $6 \times 7$. You know the answer. –  Andrej Bauer Jan 18 '13 at 7:55
I am not suggesting that you do it in Coq. I am suggesting that you write a program in lambda calculus which computes $6 \times 7$ using Church numerals. If you're up to implementing lambda calculus, this would be an easy exercise. –  Andrej Bauer Jan 19 '13 at 11:00