Soft Session Types
We show how systems of session types can enforce interactions to be bounded for all typable processes. The type system we propose is based on Lafont's soft linear logic and is strongly inspired by recent works about session types as intuitionistic linear logic formulas. Our main result is the e...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2011-08-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1108.4467v1 |
| _version_ | 1811259981402472448 |
|---|---|
| author | Paolo Di Giamberardino Ugo Dal Lago |
| author_facet | Paolo Di Giamberardino Ugo Dal Lago |
| author_sort | Paolo Di Giamberardino |
| collection | DOAJ |
| description | We show how systems of session types can enforce interactions to be bounded for all typable processes. The type system we propose is based on Lafont's soft linear logic and is strongly inspired by recent works about session types as intuitionistic linear logic formulas. Our main result is the existence, for every typable process, of a polynomial bound on the length of any reduction sequence starting from it and on the size of any of its reducts. |
| first_indexed | 2024-04-12T18:39:38Z |
| format | Article |
| id | doaj.art-5c3427708efe41cf95bae49ff662d9c1 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-12T18:39:38Z |
| publishDate | 2011-08-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-5c3427708efe41cf95bae49ff662d9c12022-12-22T03:20:49ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802011-08-0164Proc. EXPRESS 2011597310.4204/EPTCS.64.5Soft Session TypesPaolo Di GiamberardinoUgo Dal LagoWe show how systems of session types can enforce interactions to be bounded for all typable processes. The type system we propose is based on Lafont's soft linear logic and is strongly inspired by recent works about session types as intuitionistic linear logic formulas. Our main result is the existence, for every typable process, of a polynomial bound on the length of any reduction sequence starting from it and on the size of any of its reducts.http://arxiv.org/pdf/1108.4467v1 |
| spellingShingle | Paolo Di Giamberardino Ugo Dal Lago Soft Session Types Electronic Proceedings in Theoretical Computer Science |
| title | Soft Session Types |
| title_full | Soft Session Types |
| title_fullStr | Soft Session Types |
| title_full_unstemmed | Soft Session Types |
| title_short | Soft Session Types |
| title_sort | soft session types |
| url | http://arxiv.org/pdf/1108.4467v1 |
| work_keys_str_mv | AT paolodigiamberardino softsessiontypes AT ugodallago softsessiontypes |