Girard translation and logical predicates

Abstract

We present a short proof of a folklore result: the Girard translation from the simply typed lambda calculus to the linear lambda calculus is fully complete . The proof makes use of a notion of logical predicates for intuitionistic linear logic. While the main result is of independent interest, this paper can be read as a tutorial on this proof technique for reasoning about relations between type theories.