New answers tagged lambda-calculus
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 ...
Top 50 recent answers are included
Related Tags
lambda-calculus × 265type-theory × 77
lo.logic × 60
pl.programming-languages × 51
typed-lambda-calculus × 37
functional-programming × 24
computability × 18
reference-request × 17
dependent-type × 15
type-systems × 15
combinatory-logic × 15
normalization × 14
turing-machines × 12
soft-question × 11
ct.category-theory × 11
interaction-nets × 11
denotational-semantics × 10
cc.complexity-theory × 9
calculus-of-constructions × 8
big-picture × 7
term-rewriting-systems × 7
operational-semantics × 7
ho.history-overview × 6
extensionality × 6
semantics × 5