The tag has no wiki summary.

learn more… | top users | synonyms

6
votes
1answer
134 views

Simply typed lambda calculus and higher order logic

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 ...
2
votes
2answers
112 views

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 ...