Context-Free Session Types for Applied Pi-Calculus
We present a binary session type system using context-free session types to a version of the applied pi-calculus of Abadi et. al. where only base terms, constants and channels can be sent. Session types resemble process terms from BPA and we use a version of bisimulation equivalence to characterize...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2018-08-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1808.08648v1 |
| _version_ | 1818683755831754752 |
|---|---|
| author | Jens Aagaard Hans Hüttel Mathias Jakobsen Mikkel Kettunen |
| author_facet | Jens Aagaard Hans Hüttel Mathias Jakobsen Mikkel Kettunen |
| author_sort | Jens Aagaard |
| collection | DOAJ |
| description | We present a binary session type system using context-free session types to a version of the applied pi-calculus of Abadi et. al. where only base terms, constants and channels can be sent. Session types resemble process terms from BPA and we use a version of bisimulation equivalence to characterize type equivalence. We present a quotiented type system defined on type equivalence classes for which type equivalence is built into the type system. Both type systems satisfy general soundness properties; this is established by an appeal to a generic session type system for psi-calculi. |
| first_indexed | 2024-12-17T10:39:47Z |
| format | Article |
| id | doaj.art-56ad9fef30b24ed0bc809385094a5ce9 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-17T10:39:47Z |
| publishDate | 2018-08-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-56ad9fef30b24ed0bc809385094a5ce92022-12-21T21:52:16ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802018-08-01276Proc. EXPRESS/SOS 201831810.4204/EPTCS.276.3:1Context-Free Session Types for Applied Pi-CalculusJens Aagaard0Hans Hüttel1Mathias Jakobsen2Mikkel Kettunen3 Department of Computer Science, Aalborg University Department of Computer Science, Aalborg University Department of Computer Science, Aalborg University Department of Computer Science, Aalborg University We present a binary session type system using context-free session types to a version of the applied pi-calculus of Abadi et. al. where only base terms, constants and channels can be sent. Session types resemble process terms from BPA and we use a version of bisimulation equivalence to characterize type equivalence. We present a quotiented type system defined on type equivalence classes for which type equivalence is built into the type system. Both type systems satisfy general soundness properties; this is established by an appeal to a generic session type system for psi-calculi.http://arxiv.org/pdf/1808.08648v1 |
| spellingShingle | Jens Aagaard Hans Hüttel Mathias Jakobsen Mikkel Kettunen Context-Free Session Types for Applied Pi-Calculus Electronic Proceedings in Theoretical Computer Science |
| title | Context-Free Session Types for Applied Pi-Calculus |
| title_full | Context-Free Session Types for Applied Pi-Calculus |
| title_fullStr | Context-Free Session Types for Applied Pi-Calculus |
| title_full_unstemmed | Context-Free Session Types for Applied Pi-Calculus |
| title_short | Context-Free Session Types for Applied Pi-Calculus |
| title_sort | context free session types for applied pi calculus |
| url | http://arxiv.org/pdf/1808.08648v1 |
| work_keys_str_mv | AT jensaagaard contextfreesessiontypesforappliedpicalculus AT hanshuttel contextfreesessiontypesforappliedpicalculus AT mathiasjakobsen contextfreesessiontypesforappliedpicalculus AT mikkelkettunen contextfreesessiontypesforappliedpicalculus |