Tagged Questions

The tag has no wiki summary.

learn more… | top users | synonyms

2
votes
2answers
99 views

Can Curry-Howard prove a theorem from the types in your program, that has nothing to do with your program?

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