Linearly Refined Session Types

• Main Authors: Pedro Baltazar, Dimitris Mostrous, Vasco T. Vasconcelos
• Format: Article
• Language: English
• Published: Open Publishing Association 2012-11-01
• Series: Electronic Proceedings in Theoretical Computer Science
• Online Access: http://arxiv.org/pdf/1211.4099v1

Session types capture precise protocol structure in concurrent programming, but do not specify properties of the exchanged values beyond their basic type. Refinement types are a form of dependent types that can address this limitation, combining types with logical formulae that may refer to program values and can constrain types using arbitrary predicates. We present a pi calculus with assume and assert operations, typed using a session discipline that incorporates refinement formulae written in a fragment of Multiplicative Linear Logic. Our original combination of session and refinement types, together with the well established benefits of linearity, allows very fine-grained specifications of communication protocols in which refinement formulae are treated as logical resources rather than persistent truths.