What is the relation between simply typed lambda calculus and higher order logic? Under Curry-Howard it seems that simply typed lambda calculus corresponds to propositional logic. How is it related ...
Can Curry-Howard prove a theorem from the types in your program, that has nothing to do with your program? [closed]
The following link states: Curry-Howard means that any type can be interpreted as a theorem in some logical system, and any term can be interpreted as a proof of its type. This does not mean ...