Article contents
Girard translation and logical predicates
Published online by Cambridge University Press: 01 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.
- Type
- Research Article
- Information
- Copyright
- © 2000 Cambridge University Press
- 4
- Cited by
Discussions
No Discussions have been published for this article.