Sessions as Propositions
Recently, Wadler presented a continuation-passing translation from a session-typed functional language, GV, to a process calculus based on classical linear logic, CP. However, this translation is one-way: CP is more expressive than GV. We propose an extension of GV, called HGV, and give translations...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2014-06-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1406.3479v1 |
| id |
doaj-25d5bc93a6de48c7ba621546b3658263 |
|---|---|
| record_format |
Article |
| spelling |
doaj-25d5bc93a6de48c7ba621546b36582632020-11-24T23:29:58ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802014-06-01155Proc. PLACES 201491610.4204/EPTCS.155.2:10Sessions as PropositionsSam Lindley0J. Garrett Morris1 The University of Edinburgh The University of Edinburgh Recently, Wadler presented a continuation-passing translation from a session-typed functional language, GV, to a process calculus based on classical linear logic, CP. However, this translation is one-way: CP is more expressive than GV. We propose an extension of GV, called HGV, and give translations showing that it is as expressive as CP. The new translations shed light both on the original translation from GV to CP, and on the limitations in expressiveness of GV.http://arxiv.org/pdf/1406.3479v1 |
| collection |
DOAJ |
| language |
English |
| format |
Article |
| sources |
DOAJ |
| author |
Sam Lindley J. Garrett Morris |
| spellingShingle |
Sam Lindley J. Garrett Morris Sessions as Propositions Electronic Proceedings in Theoretical Computer Science |
| author_facet |
Sam Lindley J. Garrett Morris |
| author_sort |
Sam Lindley |
| title |
Sessions as Propositions |
| title_short |
Sessions as Propositions |
| title_full |
Sessions as Propositions |
| title_fullStr |
Sessions as Propositions |
| title_full_unstemmed |
Sessions as Propositions |
| title_sort |
sessions as propositions |
| publisher |
Open Publishing Association |
| series |
Electronic Proceedings in Theoretical Computer Science |
| issn |
2075-2180 |
| publishDate |
2014-06-01 |
| description |
Recently, Wadler presented a continuation-passing translation from a session-typed functional language, GV, to a process calculus based on classical linear logic, CP. However, this translation is one-way: CP is more expressive than GV. We propose an extension of GV, called HGV, and give translations showing that it is as expressive as CP. The new translations shed light both on the original translation from GV to CP, and on the limitations in expressiveness of GV. |
| url |
http://arxiv.org/pdf/1406.3479v1 |
| work_keys_str_mv |
AT samlindley sessionsaspropositions AT jgarrettmorris sessionsaspropositions |
| _version_ |
1725543386306314240 |