Linearly Refined Session Types
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...
| Main Authors: | , , |
|---|---|
| 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 |
| _version_ | 1828491468401016832 |
|---|---|
| author | Pedro Baltazar Dimitris Mostrous Vasco T. Vasconcelos |
| author_facet | Pedro Baltazar Dimitris Mostrous Vasco T. Vasconcelos |
| author_sort | Pedro Baltazar |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-11T11:02:58Z |
| format | Article |
| id | doaj.art-6a824c371de14804a2d9789e23da10f1 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-11T11:02:58Z |
| publishDate | 2012-11-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-6a824c371de14804a2d9789e23da10f12022-12-22T01:09:49ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802012-11-01101Proc. LINEARITY 2012384910.4204/EPTCS.101.4Linearly Refined Session TypesPedro BaltazarDimitris MostrousVasco T. VasconcelosSession 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.http://arxiv.org/pdf/1211.4099v1 |
| spellingShingle | Pedro Baltazar Dimitris Mostrous Vasco T. Vasconcelos Linearly Refined Session Types Electronic Proceedings in Theoretical Computer Science |
| title | Linearly Refined Session Types |
| title_full | Linearly Refined Session Types |
| title_fullStr | Linearly Refined Session Types |
| title_full_unstemmed | Linearly Refined Session Types |
| title_short | Linearly Refined Session Types |
| title_sort | linearly refined session types |
| url | http://arxiv.org/pdf/1211.4099v1 |
| work_keys_str_mv | AT pedrobaltazar linearlyrefinedsessiontypes AT dimitrismostrous linearlyrefinedsessiontypes AT vascotvasconcelos linearlyrefinedsessiontypes |