Second-order logical relations: Extended abstract

Abstract

Logical relations are a generalization of homomorphisms between models of typed lambda calculus. We define logical relations for second-order typed lambda calculus and use these relations to give a semantic characterization of second-order lambda definability. Logical relations are also used to state and prove a general representation independence theorem. Representation independence implies that the meanings of expressions do not depend on whether true is represented by 1 and false by 0, as long as all the functions that manipulate truth values are represented correctly.