New answers tagged

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 ...
gadmm's user avatar
  • 307

Top 50 recent answers are included