Booking Holidays with Linear Logic

I will present ideas for a new coordination language based on Intuitionistic Temporal Linear Logic (ITLL), extending my earlier presentation on the encoding of Reo synchronous steps into Linear Logic. This time I will show that ITLL is expressive enough to encode the (comprehensible) part of Reo. To demonstrate this, I will first give a `complete' semantics of Reo, show the encoding into ITLL, and argue its adequacy.

The advantage of the new coordination language is that it can express behaviours which cannot be (reasonably) described in existing models of Reo. I will give some examples, drawing from the Holiday Booking case study.

Even though ITLL offers a more expressive framework than what we have now, there still remains phenomona that cannot be modelled adequately. I will give some examples and suggest extensions to the that will deal with these.  

hosted by