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?
The best λ-Calculus evaluator I have found so far is:
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
* head spine reduction
* applicative order
* hybrid normal order
* hybrid applicative order
4. Has a list of pre defined abbreavtions such as
* S, K, I
* 0 - 5
5. Has source code in SML