Lectures on the Curry-Howard Isomorphism saves the day

Morten Heine B. Sørensen and Pawel Urzyczyn's Lectures on the Curry-Howard Isomorphism (mirror 1, mirror 2, errata) provides answers to two questions I asked here before:

I speculated about a complexity problem and its relation to types. On page 104 of LotCHI (92, in print), the authors note that, in the simply-typed lambda calculus, a reduction of the type inhabitation problem to the type checking problem would show that P = PSPACE.

I also wondered if there was a Heyting algebra for higher-order polymorphic typed lambda calculi that we can use to show that some type is uninhabited. LotCHI section 12.2 gets part of the way there (The authors cover F2, I would need F3, I think.), with the answer that yes, there is such an algebra, but no, it doesn't make things so easy.