–
Room P3.10, Mathematics Building
Linearly Refined Session Types
Session types capture precise protocol structure in concurrent programming, but the types remain coarse-grained in the sense that we cannot specify properties of the exchanged values beyond their basic type. Refinement types address exactly this short-coming, combining types with logical formulae that constrain the set of values of a given type, offering a more fine-grained yet logically clear specification. We present a session discipline that utilises refinement formulae written in a fragment of Multiplicative Linear Logic, expressing not only the intended specification on message types but also finer properties arising from the treatment of refinements as logical resources. [Joint work with Vasco T. Vasconcelos and Dimitris Mostrous, to be presented at LINEARITY 2012.]