Linear Lambda Calculus and PTIME-Completeness

I've just finished reading (the parts I could understand of) a paper with the same name as the title of this post, and I'm very impressed. It turns out that the linear lambda calculus has all the computing power of a boolean logic circuit and that the types in linear lambda terms uniquely determine their terms and since they are all typeable, there is an isomorphism between types and terms.

I definitely recommend the paper, especially the part where they do a simple embedding of boolean circuits in the simply typed lambda calculus and find that typing the resulting term results in the type of the embedding of true or false, which is also the normal form of the resulting lambda term. Good stuff all around!

One last cool thing- as I understood it, they also said that the type system of the simply typed lambda calculus is the linear lambda calculus. This seems to be common with systems of logic, where the upper layers are some restricted form of the lower.