Logical Relations and the Typed Lambda-Calculus