Weak Typed Boehm Theorem on IMLL

Details Weak Typed Boehm Theorem on IMLL Weak Typed Boehm Theorem on IMLL

2004-10-14

arxiv.org/abs/cs/0410030v12

Computer Science

Logic in Computer Science

a few minor corrections

Scientific paper

10.1016/j.apal.2006.06.001

In the Boehm theorem workshop on Crete island, Zoran Petric called Statman's ``Typical Ambiguity theorem'' typed Boehm theorem. Moreover, he gave a new proof of the theorem based on set-theoretical models of the simply typed lambda calculus. In this paper, we study the linear version of the typed Boehm theorem on a fragment of Intuitionistic Linear Logic. We show that in the multiplicative fragment of intuitionistic linear logic without the multiplicative unit 1 (for short IMLL) weak typed Boehm theorem holds. The system IMLL exactly corresponds to the linear lambda calculus without exponentials, additives and logical constants. The system IMLL also exactly corresponds to the free symmetric monoidal closed category without the unit object. As far as we know, our separation result is the first one with regard to these systems in a purely syntactical manner.

Affiliated with

Also associated with

No associations

Rating

Weak Typed Boehm Theorem on IMLL does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Weak Typed Boehm Theorem on IMLL, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Weak Typed Boehm Theorem on IMLL will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-664059