Precise subtyping for synchronous multiparty sessions
The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different point...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2016-02-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1602.03593v1 |
| _version_ | 1818579064484528128 |
|---|---|
| author | Mariangiola Dezani-Ciancaglini Silvia Ghilezan Svetlana Jakšić Jovanka Pantović Nobuko Yoshida |
| author_facet | Mariangiola Dezani-Ciancaglini Silvia Ghilezan Svetlana Jakšić Jovanka Pantović Nobuko Yoshida |
| author_sort | Mariangiola Dezani-Ciancaglini |
| collection | DOAJ |
| description | The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: operational and denotational. The former preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. The latter preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The result of this paper is the operational and denotational preciseness of the subtyping for a synchronous multiparty session calculus. The novelty of this paper is the introduction of characteristic global types to prove the operational completeness. |
| first_indexed | 2024-12-16T06:55:46Z |
| format | Article |
| id | doaj.art-2070fd27c86a4f6bb7f2c19c7b904218 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-16T06:55:46Z |
| publishDate | 2016-02-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-2070fd27c86a4f6bb7f2c19c7b9042182022-12-21T22:40:17ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802016-02-01203Proc. PLACES 2015294310.4204/EPTCS.203.3:3Precise subtyping for synchronous multiparty sessionsMariangiola Dezani-Ciancaglini0Silvia Ghilezan1Svetlana Jakšić2Jovanka Pantović3Nobuko Yoshida4 Università di Torino, Italy Univerzitet u Novom Sadu, Serbia Univerzitet u Novom Sadu, Serbia Univerzitet u Novom Sadu, Serbia Imperial College London, UK The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: operational and denotational. The former preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. The latter preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The result of this paper is the operational and denotational preciseness of the subtyping for a synchronous multiparty session calculus. The novelty of this paper is the introduction of characteristic global types to prove the operational completeness.http://arxiv.org/pdf/1602.03593v1 |
| spellingShingle | Mariangiola Dezani-Ciancaglini Silvia Ghilezan Svetlana Jakšić Jovanka Pantović Nobuko Yoshida Precise subtyping for synchronous multiparty sessions Electronic Proceedings in Theoretical Computer Science |
| title | Precise subtyping for synchronous multiparty sessions |
| title_full | Precise subtyping for synchronous multiparty sessions |
| title_fullStr | Precise subtyping for synchronous multiparty sessions |
| title_full_unstemmed | Precise subtyping for synchronous multiparty sessions |
| title_short | Precise subtyping for synchronous multiparty sessions |
| title_sort | precise subtyping for synchronous multiparty sessions |
| url | http://arxiv.org/pdf/1602.03593v1 |
| work_keys_str_mv | AT mariangioladezaniciancaglini precisesubtypingforsynchronousmultipartysessions AT silviaghilezan precisesubtypingforsynchronousmultipartysessions AT svetlanajaksic precisesubtypingforsynchronousmultipartysessions AT jovankapantovic precisesubtypingforsynchronousmultipartysessions AT nobukoyoshida precisesubtypingforsynchronousmultipartysessions |