Sign up ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

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:

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
* head spine reduction
* 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
* add
* mul
5. Has source code in SML

share|cite|improve this question
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
@AndrejBauer Yes I would like to verify that the evaluation works correctly for my implementation of a λ-calculus. Which theorem prover(s) are you refering to that use λ-calculus underneath? Some of us recently did this and it did not use λ-calculus. – Guy Coder Jan 18 '13 at 0:16
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
Pelletier problems test the power of ATP systems. Nowadays it is tested against TPTP. Implementation correctness is a different story. You could test random formulas against a known good implementation. – Dmitri Chubarov Jan 20 '13 at 14:04

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.