Room P3.10, Mathematics Building

Pedro Baltazar, SQIG - Instituto de Telecomunicações

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.]