New answers tagged curry-howard
2
votes
Connection between strong normalization of the simply typed λ-calculus, and cut elimination for propositional logic
How “standard” is it? A post by Anupam Das on the proof theory blog attacks the folklore by comparing the following two results:
Proposition 1 (Folklore). For any theorem A of IPL, we can compute a ...
- 307
Top 50 recent answers are included