[aufreak]

The author says that simply typed lambda calculus proves that programs terminate. That sounds to me like saying "simply typed lambda calculus is not Turing-complete". Disclaimer: I know basics of lambda calculus but don't exactly know what the "simply typed" one is.

[camccann]

You are correct, it's not. In the simply-typed lambda calculus, generally recursive constructs (such as fixed-point combinators like our friend Y) do not have valid types and are not legal.

Wikipedia has a nice article on it: http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus