Questions tagged [lambda-calculus]
Use this tag when asking a question that is not about a specific Lambda-calculus such as pure, typed, etc.
2 questions
10
votes
3
answers
342
views
Is there something special about weak head normal form used with proof assistants?
Is there something special about weak head normal form used with proof assistants?
What I am seeking does not have to be specific just something to act like a compass to give me an indication of what ...
- 2,856
2
votes
5
answers
546
views
LEM, the halting problem, the curry-howard correspondence -> deep connection?
I posted the following on the math stackexchange, but it occurs to me that this might be a more (or at least equally?) appropriate forum:
It was recently said to me by a prominent mathematician, who I ...
user3074