Girard translation and logical predicates

Masahito Hasegawa

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

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.

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

Pointers to Related Work

A. Barber and G. Plotkin, Dual Intuitionistic Linear Logic. Submitted for publication, 1997.
M. Hasegawa, Logical predicates for intuitionistic linear type theories. In Proc. TLCA'99, Springer LNCS 1581 (1999) 198-213.

Back to Hassei's Research Page / Home Page