Soft Session Types

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

Full description

Bibliographic Details
Main Authors: Paolo Di Giamberardino, Ugo Dal Lago
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
id doaj-5c3427708efe41cf95bae49ff662d9c1
record_format Article
spelling doaj-5c3427708efe41cf95bae49ff662d9c12020-11-24T20:45:54ZengOpen 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
collection DOAJ
language English
format Article
sources DOAJ
author Paolo Di Giamberardino
Ugo Dal Lago
spellingShingle Paolo Di Giamberardino
Ugo Dal Lago
Soft Session Types
Electronic Proceedings in Theoretical Computer Science
author_facet Paolo Di Giamberardino
Ugo Dal Lago
author_sort Paolo Di Giamberardino
title Soft Session Types
title_short Soft Session Types
title_full Soft Session Types
title_fullStr Soft Session Types
title_full_unstemmed Soft Session Types
title_sort soft session types
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2011-08-01
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.
url http://arxiv.org/pdf/1108.4467v1
work_keys_str_mv AT paolodigiamberardino softsessiontypes
AT ugodallago softsessiontypes
_version_ 1716813739170201600

Similar Items