I was reading http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus and I'm having a hard time thinking of anything remotely interesting that can be proven within Simply Typed lambda calculus.
Am I wrong? Or do you need dependent types to prove anything interesting.
According to same article in Wikipedia simply typed lambda calculus is equivalent to minimal logic. Maybe it can be simpler to find what can be proven by minimal logic. Then you can choose what you think is interesting.