Girard translation and logical predicates

Masahito Hasegawa

Journal of Functional Programming 10(1): 77-89, January 2000


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.

[gzipped ps file] [pdf file] [math. rev.]

Pointers to Related Work

Back to Hassei's Research Page / Home Page